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