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 let rec size_of_kind =
  40   function
  41     | Type -> 1
  42     | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
  43     | KSkip k -> size_of_kind k
  44 ;;
  45
  46 let bracket size_of pp o =
  47   if size_of o > 1 then
  48     "(" ^ pp o ^ ")"
  49   else
  50     pp o
  51 ;;
  52
  53 let rec pretty_print_kind =
  54   function
  55     | Type -> "*"
  56     | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
  57     | KSkip k -> pretty_print_kind k
  58 ;;
  59
  60 type typ =
  61   | Var of int
  62   | Unit
  63   | Top
  64   | TConst of typformerreference
  65   | Arrow of typ * typ
  66   | TSkip of typ
  67   | Forall of string * kind * typ
  68   | TAppl of typ list
  69
  70 let rec size_of_type =
  71   function
  72     | Var v -> 1
  73     | Unit -> 1
  74     | Top -> 1
  75     | TConst c -> 1
  76     | Arrow _ -> 2
  77     | TSkip t -> size_of_type t
  78     | Forall _ -> 2
  79     | TAppl l -> 1
  80 ;;
  81
  82 type term =
  83   | Rel of int
  84   | UnitTerm
  85   | Const of reference
  86   | Lambda of string * (* typ **) term
  87   | Appl of term list
  88   | LetIn of string * (* typ **) term * term
  89   | Match of reference * term * term list
  90   | TLambda of (* string **) term
  91   | Inst of (*typ_former **) term
  92   | Skip of term
  93 ;;
  94
  95 let rec size_of_term =
  96   function
  97     | Rel r -> 1
  98     | UnitTerm -> 1
  99     | Const c -> 1
 100     | Lambda (name, body) -> 1 + size_of_term body
 101     | Appl l -> List.length l
 102     | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body
 103     | Match (name, case, pats) -> 1 + size_of_term case + List.length pats
 104     | TLambda t -> size_of_term t
 105     | Inst t -> size_of_term t
 106     | Skip t -> size_of_term t
 107 ;;
 108 let unitty =
 109  NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));;
 110
 111 (* None = dropped abstraction *)
 112 type typ_context = (string * kind) option list
 113 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 114
 115 type typ_former_decl = typ_context * kind
 116 type typ_former_def = typ_former_decl * typ
 117
 118 type term_former_decl = term_context * typ
 119 type term_former_def = term_former_decl * term
 120
 121 type obj_kind =
 122    TypeDeclaration of typ_former_decl
 123  | TypeDefinition of typ_former_def
 124  | TermDeclaration of term_former_decl
 125  | TermDefinition of term_former_def
 126  | LetRec of obj_kind list
 127    (* name, left, right, constructors *)
 128  | Algebraic of (string * typ_context * typ_context * (string * typ) list) list
 129
 130 type obj = NUri.uri * obj_kind
 131
 132 let rec classify_not_term status context t =
 133  match NCicReduction.whd status ~subst:[] context t with
 134   | NCic.Sort s ->
 135      (match s with
 136          NCic.Prop
 137        | NCic.Type [`CProp,_] -> `PropKind
 138        | NCic.Type [`Type,_] -> `Kind
 139        | NCic.Type _ -> assert false)
 140   | NCic.Prod (b,s,t) ->
 141      (*CSC: using invariant on "_" *)
 142      classify_not_term status ((b,NCic.Decl s)::context) t
 143   | NCic.Implicit _
 144   | NCic.LetIn _
 145   | NCic.Lambda _
 146   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 147   | NCic.Appl [] -> assert false (* NOT POSSIBLE *)
 148   | NCic.Match _
 149   | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
 150      (* be aware: we can be the head of an application *)
 151      assert false (* TODO *)
 152   | NCic.Meta _ -> assert false (* TODO *)
 153   | NCic.Appl (he::_) -> classify_not_term status context he
 154   | NCic.Rel n ->
 155      let rec find_sort typ =
 156       match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
 157         NCic.Sort NCic.Prop -> `Proposition
 158       | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
 159       | NCic.Sort (NCic.Type [`Type,_]) ->
 160          (*CSC: we could be more precise distinguishing the user provided
 161                 minimal elements of the hierarchies and classify these
 162                 as `Kind *)
 163          `KindOrType
 164       | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
 165       | NCic.Prod (_,_,t) ->
 166          (* we skipped arguments of applications, so here we need to skip
 167             products *)
 168          find_sort t
 169       | _ -> assert false (* NOT A SORT *)
 170      in
 171       (match List.nth context (n-1) with
 172           _,NCic.Decl typ -> find_sort typ
 173         | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
 174   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
 175      let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
 176       (match classify_not_term status [] ty with
 177         | `Proposition
 178         | `Type -> assert false (* IMPOSSIBLE *)
 179         | `Kind
 180         | `KindOrType -> `Type
 181         | `PropKind -> `Proposition)
 182   | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
 183      let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
 184      let _,_,arity,_ = List.nth ityl i in
 185       (match classify_not_term status [] arity with
 186         | `Proposition
 187         | `Type
 188         | `KindOrType -> assert false (* IMPOSSIBLE *)
 189         | `Kind -> `Type
 190         | `PropKind -> `Proposition)
 191   | NCic.Const (NReference.Ref (_,NReference.Con _))
 192   | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
 193      assert false (* IMPOSSIBLE *)
 194 ;;
 195
 196 type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
 197
 198 let classify status ~metasenv context t =
 199  match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
 200   | NCic.Sort _ ->
 201      (classify_not_term status context t : not_term :> [> not_term])
 202   | ty ->
 203      let ty = fix_sorts ty in
 204       `Term
 205         (match classify_not_term status context ty with
 206           | `Proposition -> `Proof
 207           | `Type -> `Term
 208           | `KindOrType -> `TypeFormerOrTerm
 209           | `Kind -> `TypeFormer
 210           | `PropKind -> `PropFormer)
 211 ;;
 212
 213
 214 let rec kind_of status ~metasenv context k =
 215  match NCicReduction.whd status ~subst:[] context k with
 216   | NCic.Sort NCic.Type _ -> Type
 217   | NCic.Sort _ -> assert false (* NOT A KIND *)
 218   | NCic.Prod (b,s,t) ->
 219      (match classify status ~metasenv context s with
 220        | `Kind ->
 221            KArrow (kind_of status ~metasenv context s,
 222             kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
 223        | `Type
 224        | `KindOrType
 225        | `Proposition
 226        | `PropKind ->
 227            KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
 228        | `Term _ -> assert false (* IMPOSSIBLE *))
 229   | NCic.Implicit _
 230   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 231   | NCic.Lambda _
 232   | NCic.Rel _
 233   | NCic.Const _ -> assert false (* NOT A KIND *)
 234   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 235                                    otherwise NOT A KIND *)
 236   | NCic.Meta _
 237   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 238 ;;
 239
 240 let rec skip_args status ~metasenv context =
 241  function
 242   | _,[] -> []
 243   | [],_ -> assert false (* IMPOSSIBLE *)
 244   | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
 245   | _::tl1,arg::tl2 ->
 246      match classify status ~metasenv context arg with
 247       | `KindOrType
 248       | `Type
 249       | `Term `TypeFormer ->
 250          Some arg::skip_args status ~metasenv context (tl1,tl2)
 251       | `Kind
 252       | `Proposition
 253       | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
 254       | `Term _ -> assert false (* IMPOSSIBLE *)
 255 ;;
 256
 257 module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
 258
 259 type db = (typ_context * typ option) ReferenceMap.t
 260
 261 class type g_status =
 262  object
 263   method extraction_db: db
 264  end
 265
 266 class virtual status =
 267  object
 268   inherit NCic.status
 269   val extraction_db = ReferenceMap.empty
 270   method extraction_db = extraction_db
 271   method set_extraction_db v = {< extraction_db = v >}
 272   method set_extraction_status
 273    : 'status. #g_status as 'status -> 'self
 274    = fun o -> {< extraction_db = o#extraction_db >}
 275  end
 276
 277 let rec split_kind_prods context =
 278  function
 279   | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
 280   | KSkip ta -> split_kind_prods (None::context) ta
 281   | Type -> context,Type
 282 ;;
 283
 284 let rec split_typ_prods context =
 285  function
 286   | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
 287   | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
 288   | TSkip ta -> split_typ_prods (None::context) ta
 289   | _ as t -> context,t
 290 ;;
 291
 292 let rec glue_ctx_typ ctx typ =
 293  match ctx with
 294   | [] -> typ
 295   | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
 296   | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
 297   | None::ctx -> glue_ctx_typ ctx (TSkip typ)
 298 ;;
 299
 300 let rec split_typ_lambdas status n ~metasenv context typ =
 301  if n = 0 then context,typ
 302  else
 303   match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
 304    | NCic.Lambda (name,s,t) ->
 305       split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
 306    | t ->
 307       (* eta-expansion required *)
 308       let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
 309       match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
 310        | NCic.Prod (name,typ,_) ->
 311           split_typ_lambdas status (n-1) ~metasenv
 312            ((name,NCic.Decl typ)::context)
 313            (NCicUntrusted.mk_appl t [NCic.Rel 1])
 314        | _ -> assert false (* IMPOSSIBLE *)
 315 ;;
 316
 317
 318 let context_of_typformer status ~metasenv context =
 319  function
 320     NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
 321   | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
 322   | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
 323   | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
 324      (try fst (ReferenceMap.find ref status#extraction_db)
 325       with
 326        Not_found -> assert false (* IMPOSSIBLE *))
 327   | NCic.Match _ -> assert false (* TODO ???? *)
 328   | NCic.Rel n ->
 329      let typ =
 330       match List.nth context (n-1) with
 331          _,NCic.Decl typ -> typ
 332        | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
 333      let typ_ctx = snd (HExtlib.split_nth n context) in
 334      let typ = kind_of status ~metasenv typ_ctx typ in
 335       fst (split_kind_prods [] typ)
 336   | NCic.Meta _ -> assert false (* TODO *)
 337   | NCic.Const (NReference.Ref (_,NReference.Con _))
 338   | NCic.Const (NReference.Ref (_,NReference.CoFix _))
 339   | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
 340   | NCic.Appl _ | NCic.Prod _ ->
 341      assert false (* IMPOSSIBLE *)
 342
 343 let rec typ_of status ~metasenv context k =
 344  match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
 345   | NCic.Prod (b,s,t) ->
 346      (* CSC: non-invariant assumed here about "_" *)
 347      (match classify status ~metasenv context s with
 348        | `Kind ->
 349            Forall (b, kind_of status ~metasenv context s,
 350             typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
 351        | `Type
 352        | `KindOrType -> (* ??? *)
 353            Arrow (typ_of status ~metasenv context s,
 354             typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 355        | `PropKind
 356        | `Proposition ->
 357            TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
 358        | `Term _ -> assert false (* IMPOSSIBLE *))
 359   | NCic.Sort _
 360   | NCic.Implicit _
 361   | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
 362   | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *)
 363   | NCic.Rel n -> Var n
 364   | NCic.Const ref -> TConst ref
 365   | NCic.Appl (he::args) ->
 366      let he_context = context_of_typformer status ~metasenv context he in
 367      TAppl (typ_of status ~metasenv context he ::
 368       List.map
 369        (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
 370        (skip_args status ~metasenv context (List.rev he_context,args)))
 371   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 372                                    otherwise NOT A TYPE *)
 373   | NCic.Meta _
 374   | NCic.Match (_,_,_,_) -> assert false (* TODO *)
 375 ;;
 376
 377 let rec fomega_subst k t1 =
 378  function
 379   | Var n ->
 380      if k=n then t1
 381      else if n < k then Var n
 382      else Var (n-1)
 383   | Top -> Top
 384   | TConst ref -> TConst ref
 385   | Unit -> Unit
 386   | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
 387   | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
 388   | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
 389   | TAppl args -> TAppl (List.map (fomega_subst k t1) args)
 390
 391 let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
 392
 393 let rec fomega_whd status ty =
 394  match ty with
 395  | TConst r ->
 396     (match fomega_lookup status r with
 397         None -> ty
 398       | Some ty -> fomega_whd status ty)
 399  | TAppl (TConst r::args) ->
 400     (match fomega_lookup status r with
 401         None -> ty
 402       | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
 403  | _ -> ty
 404
 405 let rec term_of status ~metasenv context =
 406  function
 407   | NCic.Implicit _
 408   | NCic.Sort _
 409   | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
 410   | NCic.Lambda (b,ty,bo) ->
 411      (* CSC: non-invariant assumed here about "_" *)
 412      (match classify status ~metasenv context ty with
 413        | `Kind ->
 414            TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 415        | `KindOrType (* ??? *)
 416        | `Type ->
 417            Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 418        | `PropKind
 419        | `Proposition ->
 420            (* CSC: LAZY ??? *)
 421            Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
 422        | `Term _ -> assert false (* IMPOSSIBLE *))
 423   | NCic.LetIn (b,ty,t,bo) ->
 424      (match classify status ~metasenv context t with
 425        | `Term `TypeFormerOrTerm (* ???? *)
 426        | `Term `Term ->
 427           LetIn (b,term_of status ~metasenv context t,
 428            term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
 429        | `Kind
 430        | `Type
 431        | `KindOrType
 432        | `PropKind
 433        | `Proposition
 434        | `Term `PropFormer
 435        | `Term `TypeFormer
 436        | `Term `Proof ->
 437          (* not in programming languages, we expand it *)
 438          term_of status ~metasenv context
 439           (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
 440   | NCic.Rel n -> Rel n
 441   | NCic.Const ref -> Const ref
 442   | NCic.Appl (he::args) ->
 443      eat_args status metasenv
 444       (term_of status ~metasenv context he) context
 445       (typ_of status ~metasenv context
 446         (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
 447       args
 448 (*
 449      let he_context = context_of_typformer status ~metasenv context he in
 450      let process_args he =
 451       function
 452          `Empty -> he
 453        | `Inst tl -> Inst (process_args he tl)
 454        | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
 455      in
 456      Appl (typ_of status ~metasenv context he ::
 457       process_args (typ_of status ~metasenv context he)
 458        (skip_term_args status ~metasenv context (List.rev he_context,args))
 459 *)
 460   | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
 461                                    otherwise NOT A TYPE *)
 462   | NCic.Meta _ -> assert false (* TODO *)
 463   | NCic.Match (ref,_,t,pl) ->
 464      Match (ref,term_of status ~metasenv context t,
 465       List.map (term_of status ~metasenv context) pl)
 466 and eat_args status metasenv acc context tyhe =
 467  function
 468     [] -> acc
 469   | arg::tl ->
 470      let mk_appl f x =
 471       match f with
 472          Appl args -> Appl (args@[x])
 473        | _ -> Appl [f;x]
 474      in
 475      match fomega_whd status tyhe with
 476         Arrow (s,t) ->
 477          let arg =
 478           match s with
 479              Unit -> UnitTerm
 480            | _ -> term_of status ~metasenv context arg in
 481          eat_args status metasenv (mk_appl acc arg) context t tl
 482       | Forall (_,_,t) ->
 483          eat_args status metasenv (Inst acc)
 484           context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
 485       | TSkip t ->
 486          eat_args status metasenv acc context t tl
 487       | Top -> assert false (*TODO: HOW??*)
 488       | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
 489 ;;
 490
 491 type 'a result =
 492   | Erased
 493   | OutsideTheory
 494   | Failure of string
 495   | Success of 'a
 496 ;;
 497
 498 let object_of_constant status ~metasenv uri height bo ty =
 499   match classify status ~metasenv [] ty with
 500     | `Kind ->
 501         let ty = kind_of status ~metasenv [] ty in
 502         let ctx0,res = split_kind_prods [] ty in
 503         let ctx,bo =
 504          split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
 505         (match classify status ~metasenv ctx bo with
 506           | `Type
 507           | `KindOrType -> (* ?? no kind formers in System F_omega *)
 508               let nicectx =
 509                List.map2
 510                 (fun p1 n ->
 511                   HExtlib.map_option (fun (_,k) ->
 512                    (*CSC: BUG here, clashes*)
 513                    String.uncapitalize (fst n),k) p1)
 514                 ctx0 ctx
 515               in
 516               (* BUG here: for mutual type definitions the spec is not good *)
 517               let ref =
 518                NReference.reference_of_spec uri (NReference.Def height) in
 519               let bo = typ_of status ~metasenv ctx bo in
 520                status#set_extraction_db
 521                 (ReferenceMap.add ref (nicectx,Some bo)
 522                   status#extraction_db),
 523                Success (uri,TypeDefinition((nicectx,res),bo))
 524           | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
 525           | `PropKind
 526           | `Proposition -> status, Erased
 527           | `Term _ -> status, Failure "Body of type lambda classified as a term.  This is a bug.")
 528     | `PropKind
 529     | `Proposition -> status, Erased
 530     | `KindOrType (* ??? *)
 531     | `Type ->
 532        (* CSC: TO BE FINISHED, REF NON REGISTERED *)
 533        let ty = typ_of status ~metasenv [] ty in
 534         status,
 535         Success (uri, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
 536     | `Term _ -> status, Failure "Non-term classified as a term.  This is a bug."
 537 ;;
 538
 539 let object_of_inductive status ~metasenv uri ind leftno il =
 540  let status,_,rev_tyl =
 541   List.fold_left
 542    (fun (status,i,res) (_,name,arity,cl) ->
 543      match classify_not_term status [] arity with
 544       | `Proposition
 545       | `KindOrType
 546       | `Type -> assert false (* IMPOSSIBLE *)
 547       | `PropKind -> status,i+1,res
 548       | `Kind ->
 549           let arity = kind_of status ~metasenv [] arity in
 550           let ctx,_ = split_kind_prods [] arity in
 551           let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
 552           let ref =
 553            NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
 554           let status =
 555            status#set_extraction_db
 556             (ReferenceMap.add ref (ctx,None) status#extraction_db) in
 557           let cl =
 558            List.map
 559             (fun (_,name,ty) ->
 560               let ctx,ty =
 561                NCicReduction.split_prods status ~subst:[] [] leftno ty in
 562               let ty = typ_of status ~metasenv ctx ty in
 563                name,ty
 564             ) cl
 565           in
 566            status,i+1,(name,left,right,cl)::res
 567    ) (status,0,[]) il
 568  in
 569   match rev_tyl with
 570      [] -> status,Erased
 571    | _ -> status, Success (uri, Algebraic (List.rev rev_tyl))
 572 ;;
 573
 574 let object_of status (uri,height,metasenv,subst,obj_kind) =
 575   let obj_kind = apply_subst subst obj_kind in
 576       match obj_kind with
 577         | NCic.Constant (_,_,None,ty,_) ->
 578           (match classify status ~metasenv [] ty with
 579             | `Kind ->
 580               let ty = kind_of status ~metasenv [] ty in
 581               let ctx,_ as res = split_kind_prods [] ty in
 582               let ref = NReference.reference_of_spec uri NReference.Decl in
 583                 status#set_extraction_db
 584                   (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res)
 585             | `PropKind
 586             | `Proposition -> status, Erased
 587             | `Type
 588             | `KindOrType (*???*) ->
 589               let ty = typ_of status ~metasenv [] ty in
 590                 status, Success (uri, TermDeclaration (split_typ_prods [] ty))
 591             | `Term _ -> status, Failure "Type classified as a term.  This is a bug.")
 592         | NCic.Constant (_,_,Some bo,ty,_) ->
 593           object_of_constant status ~metasenv uri height bo ty
 594         | NCic.Fixpoint (_fix_or_cofix,fs,_) ->
 595           let status,objs =
 596             List.fold_right
 597             (fun (_,_name,_,ty,bo) (status,res) ->
 598               let status,obj = object_of_constant ~metasenv status uri height bo ty in
 599                 match obj with
 600                   | Success (_uri,obj) -> status, obj::res
 601                   | _ -> status, res) fs (status,[])
 602           in
 603             status, Success (uri,LetRec objs)
 604         | NCic.Inductive (ind,leftno,il,_) ->
 605            object_of_inductive status ~metasenv uri ind leftno il
 606
 607 (************************ HASKELL *************************)
 608
 609 (* -----------------------------------------------------------------------------
 610  * Helper functions I can't seem to find anywhere in the OCaml stdlib?
 611  * -----------------------------------------------------------------------------
 612  *)
 613 let (|>) f g =
 614   fun x -> g (f x)
 615 ;;
 616
 617 let curry f x y =
 618   f (x, y)
 619 ;;
 620
 621 let uncurry f (x, y) =
 622   f x y
 623 ;;
 624
 625 let rec char_list_of_string s =
 626   let l = String.length s in
 627   let rec aux buffer s =
 628     function
 629       | 0 -> buffer
 630       | m -> aux (s.[m - 1]::buffer) s (m - 1)
 631   in
 632     aux [] s l
 633 ;;
 634
 635 let string_of_char_list s =
 636   let rec aux buffer =
 637     function
 638       | []    -> buffer
 639       | x::xs -> aux (String.make 1 x ^ buffer) xs
 640   in
 641     aux "" s
 642 ;;
 643
 644 (* ----------------------------------------------------------------------------
 645  * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
 646  * and type variable names.
 647  * ----------------------------------------------------------------------------
 648  *)
 649
 650 let remove_underscores_and_mark =
 651   let rec aux char_list_buffer positions_buffer position =
 652     function
 653       | []    -> (string_of_char_list char_list_buffer, positions_buffer)
 654       | x::xs ->
 655         if x == '_' then
 656           aux char_list_buffer (position::positions_buffer) position xs
 657         else
 658           aux (x::char_list_buffer) positions_buffer (position + 1) xs
 659   in
 660     aux [] [] 0
 661 ;;
 662
 663 let rec capitalize_marked_positions s =
 664   function
 665     | []    -> s
 666     | x::xs ->
 667       if x < String.length s then
 668         let c = Char.uppercase (String.get s x) in
 669         let _ = String.set s x c in
 670           capitalize_marked_positions s xs
 671       else
 672         capitalize_marked_positions s xs
 673 ;;
 674
 675 let contract_underscores_and_capitalise =
 676   char_list_of_string |>
 677   remove_underscores_and_mark |>
 678   uncurry capitalize_marked_positions
 679 ;;
 680
 681 let idiomatic_haskell_type_name_of_string =
 682   contract_underscores_and_capitalise |>
 683   String.capitalize
 684 ;;
 685
 686 let idiomatic_haskell_term_name_of_string =
 687   contract_underscores_and_capitalise |>
 688   String.uncapitalize
 689 ;;
 690
 691 (*CSC: code to be changed soon when we implement constructors and
 692   we fix the code for term application *)
 693 let classify_reference status ref =
 694   if ReferenceMap.mem ref status#extraction_db then
 695     `TypeName
 696   else
 697     `FunctionName
 698 ;;
 699
 700 let capitalize classification name =
 701   match classification with
 702     | `Constructor
 703     | `TypeName -> idiomatic_haskell_type_name_of_string name
 704     | `FunctionName -> idiomatic_haskell_term_name_of_string name
 705 ;;
 706
 707 let pp_ref status ref =
 708  capitalize (classify_reference status ref)
 709   (NCicPp.r2s status false ref)
 710
 711 let name_of_uri classification uri =
 712  capitalize classification (NUri.name_of_uri uri)
 713
 714 (* cons avoid duplicates *)
 715 let rec (@:::) name l =
 716  if name <> "" (* propositional things *) && name.[0] = '_' then
 717   let name = String.sub name 1 (String.length name - 1) in
 718   let name = if name = "" then "a" else name in
 719    name @::: l
 720  else if List.mem name l then (name ^ "'") @::: l
 721  else name,l
 722 ;;
 723
 724 let (@::) x l = let x,l = x @::: l in x::l;;
 725
 726 let rec pretty_print_type status ctxt =
 727   function
 728     | Var n -> List.nth ctxt (n-1)
 729     | Unit -> "()"
 730     | Top -> assert false (* ??? *)
 731     | TConst ref -> pp_ref status ref
 732     | Arrow (t1,t2) ->
 733         bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
 734          pretty_print_type status ("_"::ctxt) t2
 735     | TSkip t -> pretty_print_type status ("_"::ctxt) t
 736     | Forall (name, kind, t) ->
 737       (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
 738       let name = String.uncapitalize name in
 739         if size_of_kind kind > 1 then
 740           "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name@::ctxt) t
 741         else
 742           "forall " ^ name ^ ". " ^ pretty_print_type status (name@::ctxt) t
 743    | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl)
 744
 745 let rec pretty_print_term status ctxt =
 746   function
 747     | Rel n -> List.nth ctxt (n-1)
 748     | UnitTerm -> "()"
 749     | Const ref -> pp_ref status ref
 750     | Lambda (name,t) -> "\\" ^ name ^ " -> " ^ pretty_print_term status (name@::ctxt) t
 751     | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
 752     | LetIn (name,s,t) ->
 753       "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t
 754     | Match (r,matched,pl) ->
 755       if pl = [] then
 756        "error \"Case analysis over empty type\""
 757       else
 758       let constructors, leftno =
 759       let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
 760       let _,_,_,cl  = List.nth tys n in
 761         cl,leftno
 762       in
 763         let rec eat_branch n ty pat =
 764           match (ty, pat) with
 765           | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat
 766           | NCic.Prod (_, _, t), Lambda (name, t') ->
 767             (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
 768             let cv, rhs = eat_branch 0 t t' in
 769               name :: cv, rhs
 770           | _, _ -> [], pat
 771         in
 772           let j = ref 0 in
 773           let patterns =
 774             try
 775               List.map2
 776                 (fun (_, name, ty) pat -> incr j; name, eat_branch leftno ty pat) constructors pl
 777             with Invalid_argument _ -> assert false
 778           in
 779             "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^
 780               String.concat "\n"
 781                 (List.map
 782                   (fun (name,(bound_names,rhs)) ->
 783                     let pattern,body =
 784                     (*CSC: BUG avoid name clashes *)
 785                     String.concat " " (String.capitalize name::bound_names),
 786                       pretty_print_term status ((List.rev bound_names)@ctxt) rhs
 787                     in
 788                       "  " ^ pattern ^ " -> " ^ body
 789                   ) patterns)
 790     | Skip t
 791     | TLambda t -> pretty_print_term status (""@::ctxt) t
 792     | Inst t -> pretty_print_term status ctxt t
 793 ;;
 794
 795 (*
 796 type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
 797
 798 type term_former_def = term_context * term * typ
 799 type term_former_decl = term_context * typ
 800 *)
 801
 802 let rec pp_obj status (uri,obj_kind) =
 803   let pretty_print_context ctx =
 804     String.concat " " (List.rev (snd
 805       (List.fold_right
 806        (fun (x,kind) (l,res) ->
 807          let x,l = x @:::l in
 808          if size_of_kind kind > 1 then
 809           x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
 810          else
 811           x::l,x::res)
 812        (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
 813   in
 814  let namectx_of_ctx ctx =
 815   List.fold_right (@::)
 816    (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
 817  match obj_kind with
 818    TypeDeclaration (ctx,_) ->
 819     (* data?? unsure semantics: inductive type without constructor, but
 820        not matchable apparently *)
 821     if List.length ctx = 0 then
 822       "data " ^ name_of_uri `TypeName uri
 823     else
 824       "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx
 825  | TypeDefinition ((ctx, _),ty) ->
 826     let namectx = namectx_of_ctx ctx in
 827     if List.length ctx = 0 then
 828       "type " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty
 829     else
 830       "type " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
 831  | TermDeclaration (ctx,ty) ->
 832     let name = name_of_uri `FunctionName uri in
 833       name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
 834       name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
 835  | TermDefinition ((ctx,ty),bo) ->
 836     let name = name_of_uri `FunctionName uri in
 837     let namectx = namectx_of_ctx ctx in
 838     (*CSC: BUG here *)
 839     name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
 840     name ^ " = " ^ pretty_print_term status namectx bo
 841  | LetRec l ->
 842     (*CSC: BUG always uses the name of the URI *)
 843     String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
 844  | Algebraic il ->
 845     String.concat "\n"
 846      (List.map
 847       (fun _name,left,right,cl ->
 848         (*CSC: BUG always uses the name of the URI *)
 849         "data " ^ name_of_uri `TypeName uri ^ " " ^
 850         pretty_print_context (right@left) ^ " where\n  " ^
 851         String.concat "\n  " (List.map
 852          (fun name,tys ->
 853            let namectx = namectx_of_ctx left in
 854             capitalize `Constructor name ^ " :: " ^
 855              pretty_print_type status namectx tys
 856          ) cl
 857       )) il)
 858  (* inductive and records missing *)
 859
 860 let haskell_of_obj status (uri,_,_,_,_ as obj) =
 861  let status, obj = object_of status obj in
 862   status,
 863    match obj with
 864       Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n"
 865     | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n"
 866     | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n"
 867     | Success o -> pp_obj status o ^ "\n"