Proofrecording/diffs/proofobjects_coq.ml

   1 (* ======================================================================================== *)
   2 (*                 Proof-objects for HOL-light, exportation to Coq                          *)
   3 (*                                                                                          *)
   4 (*       Steven Obua, TU Mnchen, December 2004                                              *)
   5 (*       Chantal Keller, Laboratoire d'Informatique de Polytechnique (France), January 2010 *)
   6 (*                                                                                          *)
   7 (*       based on Sebastian Skalberg's HOL4 proof-objects                                   *)
   8 (* ======================================================================================== *)
   9
  10 #load "unix.cma";;
  11 #load "depgraph.cma";;
  12
  13
  14 module type Proofobject_primitives =
  15   sig
  16
  17     type proof
  18
  19     val proof_REFL : term -> proof
  20     val proof_TRANS : proof * proof -> proof
  21     val proof_MK_COMB : proof * proof -> proof
  22     val proof_ASSUME : term -> proof
  23     val proof_EQ_MP : proof -> proof -> proof
  24     val proof_IMPAS : proof -> proof -> proof
  25     val proof_DISCH : proof -> term -> proof
  26     val proof_DEDUCT_ANTISYM_RULE : proof * term -> proof * term -> proof
  27     val proof_BETA : term -> proof
  28     val proof_ABS : term -> proof -> proof
  29     val proof_INST_TYPE : (hol_type * hol_type) list -> proof -> proof
  30     val proof_INST : (term * term) list -> proof -> proof
  31     val proof_new_definition : string -> hol_type -> term -> proof
  32     val proof_CONJ : proof -> proof -> proof
  33     val proof_CONJUNCT1 : proof -> proof
  34     val proof_CONJUNCT2 : proof -> proof
  35     val proof_new_basic_type_definition :
  36       string -> string * string -> term * term -> proof -> proof
  37     val proof_SPEC : term -> proof -> proof
  38     val proof_SYM : proof -> proof
  39     val proof_GEN : proof -> term -> proof
  40     val proof_DISJ1 : proof -> term -> proof
  41     val proof_DISJ2 : proof -> term -> proof
  42     val proof_NOTI : proof -> proof
  43     val proof_NOTE : proof -> proof
  44     val proof_CONTR : proof -> term -> proof
  45     val proof_DISJCASES : proof -> proof -> proof -> proof
  46     val proof_CHOOSE : term -> proof -> proof -> proof
  47     val proof_EXISTS : term -> term -> proof -> proof
  48
  49     val new_axiom_name : string -> string
  50     val proof_new_axiom : string -> term -> proof
  51
  52     val save_proof : string -> proof -> (term option) -> unit
  53     val proof_database : unit -> ((string * proof * (term option)) list)
  54
  55     val export_saved_proofs : unit -> unit
  56     val export_one_proof : string -> unit
  57     val export_list : string list -> unit
  58   end;;
  59
  60
  61 module Proofobjects : Proofobject_primitives = struct
  62
  63
  64   let THEORY_NAME = "hollight";;
  65
  66
  67
  68   (****** Utilities ******)
  69
  70   (* this is a little bit dangerous, because the function is not injective,
  71      but I guess one can live with that *)
  72   let modify = function
  73     | "/" -> "_slash_"
  74     | "\\" -> "_backslash_"
  75     | "=" -> "_equal_"
  76     | ">" -> "_greaterthan_"
  77     | "<" -> "_lessthan_"
  78     | "?" -> "_questionmark_"
  79     | "!" -> "_exclamationmark_"
  80     | "*" -> "_star_"
  81     | "~" -> "_tilde_"
  82     | "," -> "_comma_"
  83     | "@" -> "_at_"
  84     | "+" -> "_plus_"
  85     | "-" -> "_minus_"
  86     | "%" -> "_percent_"
  87     | "$" -> "_dollar_"
  88     | "." -> "_dot_"
  89     | "'" -> "_quote_"
  90     | "|" -> "_pipe_"
  91     | ":" -> "_colon_"
  92     | s -> s;;
  93
  94   let mfc s = implode (map modify (explode s));;
  95
  96   let ensure_export_directory thyname =
  97     let dir = Sys.getenv "HOLPROOFEXPORTDIR" in
  98     let dirsub = Filename.concat dir "hollight" in
  99     let dirsubsub = Filename.concat dirsub thyname in
 100     let mk d = if Sys.file_exists d then () else Unix.mkdir d 509
 101     in mk dir; mk dirsub; mk dirsubsub; dirsubsub;;
 102
 103
 104   (****** Proofs ******)
 105
 106   type proof_info_rec =
 107       {disk_info: (string * string) option ref;
 108        status: int ref;
 109        references: int ref;
 110        queued: bool ref};;
 111
 112   type proof_info = Info of proof_info_rec;;
 113
 114   type proof =
 115     | Proof of (proof_info * proof_content * (unit -> unit))
 116   and proof_content =
 117     | Prefl of term
 118     | Pbeta of string * hol_type * term
 119     | Pinstt of proof * (string * hol_type) list
 120     | Pabs of proof * string * hol_type
 121     | Pdisch of proof * term
 122     | Phyp of term
 123     | Pspec of proof * term
 124     | Pinst of proof * (string * hol_type * term) list
 125     | Pgen of proof * string * hol_type
 126     | Psym of proof
 127     | Ptrans of proof * proof
 128     | Pcomb of proof * proof
 129     | Peqmp of proof * proof
 130     | Pexists of proof * term * term
 131     | Pchoose of string * hol_type * proof * proof
 132     | Pconj of proof * proof
 133     | Pconjunct1 of proof
 134     | Pconjunct2 of proof
 135     | Pdisj1 of proof * term
 136     | Pdisj2 of proof * term
 137     | Pdisjcases of proof * proof * proof
 138     | Pnoti of proof
 139     | Pnote of proof
 140     | Pcontr of proof * term
 141     | Pimpas of proof * proof
 142     | Paxm of string * term
 143     | Pdef of string * hol_type * term
 144     | Ptyintro of hol_type * string * hol_type list * string * string * term;;
 145
 146   let content_of (Proof (_,p,_)) = p;;
 147
 148   let inc_references (Proof(Info{references=r},_,_) as p) = incr r; p;;
 149
 150   let mk_proof p = Proof(Info {disk_info = ref None; status = ref 0; references = ref 0; queued = ref false}, p, fun () -> ());;
 151
 152   let global_ax_counter = let counter = ref 1 in let f = fun () -> (incr counter; !counter - 1) in f;;
 153
 154   let new_axiom_name n = "ax_"^n^"_"^(string_of_int (global_ax_counter () ));;
 155
 156
 157   (* corresponds to REFL *)
 158
 159   let proof_REFL t = mk_proof (Prefl t);;
 160
 161
 162   (* corresponds to TRANS, with a simple improvment *)
 163
 164   let proof_TRANS (p,q) =
 165     match (content_of p, content_of q) with
 166       | (Prefl _,_) -> q
 167       | (_, Prefl _) -> p
 168       | _ -> mk_proof (Ptrans (inc_references p, inc_references q));;
 169
 170
 171   (* corresponds to MK_COMB -> Pcomb *)
 172
 173   let proof_MK_COMB (p1,p2) =
 174     match (content_of p1, content_of p2) with
 175       | (Prefl tm1, Prefl tm2) -> mk_proof (Prefl (mk_comb (tm1, tm2)))
 176       | _ ->  mk_proof (Pcomb (inc_references p1, inc_references p2));;
 177
 178
 179   (* corresponds to ASSUME -> Phyp *)
 180
 181   let proof_ASSUME t = mk_proof (Phyp t);;
 182
 183
 184   (* corresponds to EQ_MP, with a simple improvment *)
 185
 186   let proof_EQ_MP p q =
 187     match content_of p with
 188       | Prefl _ -> q
 189       | _ -> mk_proof (Peqmp(inc_references p, inc_references q));;
 190
 191
 192   (* corresponds to IMP_ANTISYM_RULE th1 th2
 193      not a base rule
 194      used only in the extended mode *)
 195
 196   (*  A1 |- t1 ==> t2     A2 |- t2 ==> t1 *)
 197   (* ------------------------------------- IMP_ANTISYM_RULE *)
 198   (*          A1 u A2 |- t1 <=> t2 *)
 199
 200   let proof_IMPAS p1 p2 = mk_proof (Pimpas (inc_references p1, inc_references p2));;
 201
 202
 203   (* corresponds to DISCH
 204      not a base rule
 205      used only in the extended mode *)
 206
 207   (*        A |- t *)
 208   (* -------------------- DISCH `u` *)
 209   (*  A - {u} |- u ==> t *)
 210
 211   let proof_DISCH p t = mk_proof (Pdisch(inc_references p, t));;
 212
 213
 214   (* corresponds to DEDUCT_ANTISYM_RULE *)
 215   (* made with IMPAS and DISCH (whereas in HOL-Light IMPAS is made with DAR and UNDISCH...) *)
 216
 217   (*       A |- p       B |- q *)
 218   (* ---------------------------------- *)
 219   (*  (A - {q}) u (B - {p}) |- p <=> q *)
 220
 221   let proof_DEDUCT_ANTISYM_RULE (p1,t1) (p2,t2) =
 222     proof_IMPAS (proof_DISCH p1 t2) (proof_DISCH p2 t1);;
 223
 224
 225   (* BETA is a base rule *)
 226
 227   let proof_BETA tm =
 228     try
 229       let f,_ = dest_comb tm in
 230       let v,bod = dest_abs f in
 231       let (x, ty) = dest_var v in
 232       mk_proof (Pbeta (x, ty, bod))
 233     with
 234       | _ -> failwith "proof_BETA"
 235
 236
 237   (* corresponds to ABS, with a simple improvment *)
 238
 239   let proof_ABS x p =
 240     match x with
 241       | Var(s, ty) ->
 242           mk_proof (Pabs(inc_references p, s, ty))
 243       | _ -> failwith "proof_ABS: not a variable";;
 244
 245
 246   (* corresponds to INST_TYPE -> Pinstt *)
 247
 248   let proof_INST_TYPE s p =
 249     mk_proof (Pinstt(inc_references p, List.map (
 250                        fun (ty1, ty2) -> match ty2 with
 251                          | Tyvar s -> (s, ty1)
 252                          | _ -> failwith "proof_INST_TYPE: some redex is not a type variable"
 253                      ) s));;
 254
 255
 256   (* corresponds to INST *)
 257
 258   let proof_INST s p =
 259     mk_proof (Pinst(inc_references p, List.map (
 260                       fun (t1, t2) -> match t2 with
 261                         | Var(s, ty) ->
 262                             (s, ty, t1)
 263                         | _ -> failwith "proof_INST: some redex is not a term variable"
 264                     ) s));;
 265
 266
 267   (* proof_new_definition is called in Thm.new_basic_definition. This
 268      latter helps to define basic concepts such as T, AND... (almost
 269      everything in Bool)... and to define derived rules!! -> Pdef *)
 270
 271   let proof_new_definition cname ty t =
 272     mk_proof (Pdef (cname, ty, t));;
 273
 274
 275   (* proof_new_axiom is called in Thm.new_axiom. This latter transforms
 276      a term of type bool into a theorem. The main three axioms are
 277      ETA_AX, SELECT_AX and INFINITY_AX. The other axiom is ax (in
 278      drule.ml) -> Paxm *)
 279
 280   let proof_new_axiom axname t = mk_proof (Paxm (axname, t));;
 281
 282
 283   (* corresponds to CONJ
 284      not a base rule
 285      used only in the extended mode *)
 286
 287   let proof_CONJ p1 p2 = mk_proof (Pconj (inc_references p1, inc_references p2));;
 288
 289
 290   (* corresponds to CONJUNCT1
 291      not a base rule
 292      used only in the extended mode
 293      also used in Thm.new_basic_definition *)
 294
 295   let proof_CONJUNCT1 p = mk_proof (Pconjunct1 (inc_references p));;
 296
 297
 298   (* corresponds to CONJUNCT2
 299      not a base rule
 300      used only in the extended mode
 301      also used in Thm.new_basic_definition *)
 302
 303   let proof_CONJUNCT2 p = mk_proof (Pconjunct2 (inc_references p));;
 304
 305
 306   (* used only in Thm.new_basic_definition for the same purpose as for
 307      CONJUNCTi -> Ptyintro *)
 308
 309   let proof_new_basic_type_definition tyname (absname, repname) (pt,tt) _ =
 310     let rty = type_of tt in
 311     let tyvars = sort (<=) (type_vars_in_term pt) in
 312
 313     mk_proof(Ptyintro(rty, tyname, tyvars, absname, repname, pt));;
 314
 315
 316   (* ---- used only in substitute_proof calls ---- *)
 317
 318   (* corresponds to Bool.SPEC, the !-elimination rule *)
 319
 320   let proof_SPEC s p = mk_proof (Pspec(inc_references p, s));;
 321
 322
 323   (* corresponds to Equal.SYM, the symmetry rule *)
 324
 325   let proof_SYM p = mk_proof (Psym(inc_references p));;
 326
 327
 328   (* corresponds to Bool.GEN, the !-introduction rule *)
 329
 330   let proof_GEN p a =
 331     match a with
 332       | Var(s, ty) ->
 333           mk_proof (Pgen(inc_references p, s, ty))
 334       | _ -> failwith "proof_GEN: not a term variable";;
 335
 336
 337   (* corresponds to Bool.DISJ1, the \/-left introduction rule *)
 338
 339   let proof_DISJ1 p a = mk_proof (Pdisj1 (inc_references p, a));;
 340
 341
 342   (* corresponds to Bool.DISJ2, the \/-right introduction rule *)
 343
 344   let proof_DISJ2 p a = mk_proof (Pdisj2 (inc_references p, a));;
 345
 346
 347   (* corresponds to Bool.NOT_INTRO, the following rule: *)
 348   (*     A |- t ==> F *)
 349   (*    --------------  NOT_INTRO *)
 350   (*       A |- ~t *)
 351
 352   let proof_NOTI p = mk_proof (Pnoti (inc_references p));;
 353
 354
 355   (* corresponds to Bool.NOT_ELIM, the following rule: *)
 356   (*       A |- ~t *)
 357   (*    --------------  NOT_ELIM *)
 358   (*     A |- t ==> F *)
 359
 360   let proof_NOTE p = mk_proof (Pnote (inc_references p));;
 361
 362
 363   (* corresponds to Bool.CONTR, the intuitionistic F-elimination rule: *)
 364   (*     A |- F *)
 365   (*    --------  CONTR `t` *)
 366   (*     A |- t *)
 367
 368   let proof_CONTR p a = mk_proof (Pcontr (inc_references p, a));;
 369
 370
 371   (* corresponds to Bool.DISJ_CASES, the \/-elimination rule: *)
 372   (*     A |- t1 \/ t2     A1 u {t1} |- t      A2 u {t2} |- t *)
 373   (*    ------------------------------------------------------  DISJ_CASES *)
 374   (*                     A u A1 u A2 |- t *)
 375
 376   let proof_DISJCASES p q r =
 377     mk_proof (Pdisjcases (inc_references p, inc_references q, inc_references r));;
 378
 379
 380   (* corresponds to Bool.CHOOSE, the ?-elimination rule: *)
 381   (*     A1 |- ?x. s[x]    A2 |- t *)
 382   (*    -------------------------------  CHOOSE (`v`,(A1 |- ?x. s)) *)
 383   (*      A1 u (A2 - {s[v/x]}) |- t *)
 384   (* Where v is not free in A2 - {s[v/x]} or t. *)
 385
 386   let proof_CHOOSE a p q =
 387     let (x,ty) = dest_var a in
 388     mk_proof (Pchoose (x, ty, inc_references p, inc_references q));;
 389
 390
 391   (* corresponds to Bool.EXISTS, the ?-introduction rule: *)
 392   (*     A |- p[u/x] *)
 393   (*    -------------  EXISTS (`?x. p`,`u`) *)
 394   (*     A |- ?x. p *)
 395   (* x is p, y is u *)
 396
 397   let proof_EXISTS etm y p  =
 398     let _,x = dest_comb etm in
 399     mk_proof (Pexists (inc_references p, x, y));;
 400
 401
 402   (****** Utilities for exportation ******)
 403
 404   let content_of (Proof (_,x,_)) = x;;
 405
 406
 407   let disk_info_of (Proof(Info {disk_info=di},_,_)) = !di;;
 408
 409
 410   let set_disk_info_of (Proof(Info {disk_info=di},_,_)) thyname thmname =
 411     di := Some (thyname,thmname);;
 412
 413   let reset_disk_info_of1 ((Proof(Info {disk_info=di}, _, _)) as p) =
 414     di := None; p;;
 415   let reset_disk_info_of2 (Proof(Info {disk_info=di}, _, _)) =
 416     di := None;;
 417
 418
 419   let references (Proof (Info info,_,_)) = !(info.references);;
 420
 421
 422   let glob_counter = ref 0;;
 423
 424
 425   let get_counter () = incr glob_counter; !glob_counter;;
 426
 427
 428   let get_iname = string_of_int o get_counter;;
 429
 430
 431   let next_counter () = !glob_counter;;
 432
 433
 434   let trivial p =
 435     match (content_of p) with
 436       | Prefl _ -> true
 437       | Pbeta _ -> true
 438       | Paxm _ -> true
 439       | Phyp _ -> true
 440       | _ -> false;;
 441
 442
 443   let do_share p = references p > 1 & not (trivial p);;
 444
 445
 446   (****** Types and terms modification ******)
 447
 448   let  idT = Hashtbl.create 17;;
 449   let defT = Hashtbl.create 17;;
 450
 451   let  idT_ref = ref 1;;
 452   let defT_ref = ref 1;;
 453
 454   let make_idT x =
 455     try Hashtbl.find idT x with | Not_found -> let n = !idT_ref in incr idT_ref; Hashtbl.add idT x n; n;;
 456
 457   let make_defT x =
 458     try Hashtbl.find defT x with | Not_found -> let n = !defT_ref in incr defT_ref; Hashtbl.add defT x n; n;;
 459
 460
 461   type ntype =
 462     | Ntvar of int
 463     | Nbool
 464     | Nnum
 465     | Narrow of ntype * ntype
 466     | Ntdef of int * ntype list;;
 467
 468
 469   let rec hol_type2ntype = function
 470     | Tyvar x -> Ntvar (make_idT x)
 471     | Tyapp (s, _) when s = "bool" -> Nbool
 472     (* | Tyapp (s, _) when s = "ind" -> Nnum *)
 473     | Tyapp (s, l) when s = "fun" ->
 474         (match l with
 475            | [a;b] -> Narrow (hol_type2ntype a, hol_type2ntype b)
 476            | _ -> failwith "hol_type2ntype: wrong number of arguments for fun")
 477     | Tyapp (s, l) -> Ntdef (make_defT s, List.map hol_type2ntype l);;
 478
 479
 480   let  idV = Hashtbl.create 17;;
 481   let defV = Hashtbl.create 17;;
 482
 483   let  idV_ref = ref 1;;
 484   let defV_ref = ref 1;;
 485
 486   let make_idV x X =
 487     try
 488       fst (Hashtbl.find idV x)
 489     with | Not_found ->
 490       let n = !idV_ref in incr idV_ref; Hashtbl.add idV x (n,X); n;;
 491
 492   let make_defV x X f =
 493     try let (a,_,_) = (Hashtbl.find defV x) in a with | Not_found -> let n = !defV_ref in incr defV_ref; Hashtbl.add defV x (n,X,f); n;;
 494
 495
 496   type ncst =
 497     | Heq of ntype
 498     | Heps of ntype
 499     | Hand
 500     | Hor
 501     | Hnot
 502     | Himp
 503     | Htrue
 504     | Hfalse
 505     | Hforall of ntype
 506     | Hexists of ntype;;
 507
 508
 509   type nterm =
 510     | Ndbr of int
 511     | Nvar of int * ntype
 512     | Ncst of ncst
 513     | Ndef of int * ntype
 514     | Napp of nterm * nterm
 515     | Nabs of ntype * nterm;;
 516
 517
 518   let rec ext_var x (ty: ntype) i = function
 519     | [] -> Nvar (make_idV x ty, ty)
 520     | (y,typ)::l -> if ((x = y) && (ty = typ)) then Ndbr i else ext_var x ty (i+1) l;;
 521
 522
 523   let rec term2nterm l = function
 524     | Var (x, ty) -> ext_var x (hol_type2ntype ty) 0 l
 525     | Comb (t1, t2) -> Napp (term2nterm l t1, term2nterm l t2)
 526     | Abs (t1, t2) ->
 527         (match t1 with
 528            | Var (x, ty) ->
 529                let typ = hol_type2ntype ty in
 530                Nabs (typ, term2nterm ((x,typ)::l) t2)
 531            | _ -> failwith "term2nterm: first argument of an abstraction is not a variable")
 532     | Const (s, ty) when s = "=" ->
 533         (match hol_type2ntype ty with
 534            | Narrow(a, _) -> Ncst (Heq a)
 535            | _ -> failwith "term2nterm: constant = must have arrow type")
 536     | Const (s, ty) when s = "@" ->
 537         (match hol_type2ntype ty with
 538            | Narrow(_, a) -> Ncst (Heps a)
 539            | _ -> failwith "term2nterm: constant @ must have arrow type")
 540     | Const (s, ty) when s = "/\\" -> Ncst Hand
 541     | Const (s, ty) when s = "\\/" -> Ncst Hor
 542     | Const (s, ty) when s = "~" -> Ncst Hnot
 543     | Const (s, ty) when s = "==>" -> Ncst Himp
 544     | Const (s, ty) when s = "T" -> Ncst Htrue
 545     | Const (s, ty) when s = "F" -> Ncst Hfalse
 546     | Const (s, ty) when s = "_FALSITY_" -> Ncst Hfalse
 547     | Const (s, ty) when s = "!" ->
 548         (match hol_type2ntype ty with
 549            | Narrow(Narrow (a, _), _) -> Ncst (Hforall a)
 550            | _ -> failwith "term2nterm: constant ! must have arrow type")
 551     | Const (s, ty) when s = "?" ->
 552         (match hol_type2ntype ty with
 553            | Narrow(Narrow (a, _), _) -> Ncst (Hexists a)
 554            | _ -> failwith "term2nterm: constant ? must have arrow type")
 555     | Const (s, ty) ->
 556         let typ = hol_type2ntype ty in
 557         Ndef(make_defV s typ true, typ);;
 558
 559   let term2nterm t = term2nterm [] t;;
 560
 561
 562   (****** Proof exportation ******)
 563
 564   let rec print_list out str snil scons = function
 565     | [] -> out snil
 566     | t::q -> out "("; out scons; out " "; str t; out " "; print_list out str snil scons q; out ")";;
 567
 568
 569   let print_names out x = out (string_of_int x); out "%positive";;
 570
 571
 572   let print_type (out: string -> unit) ty =
 573
 574     let rec print_ntype = function
 575       | Ntvar x -> out "(TVar "; print_names out x; out ")"
 576       | Nbool -> out "Bool"
 577       | Nnum -> out "Num"
 578       | Narrow(a, b) -> out "("; print_ntype a; out " --> "; print_ntype b; out ")"
 579       | Ntdef(s, l) -> out "(TDef "; print_names out s; out " "; print_list out print_ntype "Tnil" "Tcons" l; out ")" in
 580
 581     print_ntype ty;;
 582
 583
 584   let print_cst out = function
 585     | Heq ty -> out "(Heq "; print_type out ty; out ")"
 586     | Heps ty -> out "(Heps "; print_type out ty; out ")"
 587     | Hand -> out "Hand"
 588     | Hor -> out "Hor"
 589     | Hnot -> out "Hnot"
 590     | Himp -> out "Himp"
 591     | Htrue -> out "Htrue"
 592     | Hfalse -> out "Hfalse"
 593     | Hforall ty -> out "(Hforall "; print_type out ty; out ")"
 594     | Hexists ty -> out "(Hexists "; print_type out ty; out ")";;
 595
 596
 597   let print_term out t =
 598
 599     let rec print_nterm = function
 600       | Ndbr n -> out "(Dbr "; out (string_of_int n); out ")"
 601       | Nvar(x, ty) -> out "(Var "; print_names out x; out " "; print_type out ty; out ")"
 602       | Ncst c -> out "(Cst "; print_cst out c; out ")"
 603       | Ndef(a, ty) -> out "(Def "; print_names out a; out " "; print_type out ty; out ")"
 604       | Napp(t1, t2) -> out "(App "; print_nterm t1; out " "; print_nterm t2; out ")"
 605       | Nabs(ty, t) -> out "(Abs "; print_type out ty; out " "; print_nterm t; out ")" in
 606
 607     print_nterm t;;
 608
 609
 610   (* Exportation *)
 611
 612   let total = ref 0;;
 613
 614   type nproof_content =
 615     | Nprefl of nterm
 616     | Npbeta of int * ntype * nterm
 617     | Npinstt of nproof_content * (int * ntype) list
 618     | Npabs of nproof_content * int * ntype
 619     | Npdisch of nproof_content * nterm
 620     | Nphyp of nterm
 621     | Npspec of nproof_content * nterm
 622     | Npinst of nproof_content * (int * ntype * nterm) list
 623     | Npgen of nproof_content * int * ntype
 624     | Npsym of nproof_content
 625     | Nptrans of nproof_content * nproof_content
 626     | Npcomb of nproof_content * nproof_content
 627     | Npeqmp of nproof_content * nproof_content
 628     | Npexists of nproof_content * nterm * nterm
 629     | Npchoose of int * ntype * nproof_content * nproof_content
 630     | Npconj of nproof_content * nproof_content
 631     | Npconjunct1 of nproof_content
 632     | Npconjunct2 of nproof_content
 633     | Npdisj1 of nproof_content * nterm
 634     | Npdisj2 of nproof_content * nterm
 635     | Npdisjcases of nproof_content * nproof_content * nproof_content
 636     | Npnoti of nproof_content
 637     | Npnote of nproof_content
 638     | Npcontr of nproof_content * nterm
 639     | Npimpas of nproof_content * nproof_content
 640     | Npaxm of string * nterm
 641     | Npdef of int * ntype * nterm
 642     | Nptyintro of ntype * ntype * int * int * nterm
 643     | Nfact of string;;
 644
 645
 646   let the_types = Hashtbl.create 17;;
 647   let count_types = ref (-1);;
 648
 649   let share_types out ty =
 650
 651     let rec share_types ty =
 652       try Hashtbl.find the_types ty with
 653         | Not_found ->
 654             incr count_types;
 655             let name = THEORY_NAME^"_type_"^(string_of_int !count_types) in
 656             (match ty with
 657                | Narrow(a,b) ->
 658                    let n1 = share_types a in
 659                    let n2 = share_types b in
 660                    out "\nDefinition "; out name; out " := "; out n1; out " --> "; out n2; out "."
 661                | Ntdef(i,l) ->
 662                    let names = List.map share_types l in
 663                    out "\nDefinition "; out name; out " := TDef "; print_names out i; out " "; print_list out out "Tnil" "Tcons" names; out "."
 664                | t -> out "\nDefinition "; out name; out " := "; print_type out t; out ".");
 665             Hashtbl.add the_types ty name;
 666             name in
 667
 668     share_types ty;;
 669
 670
 671   let the_terms = Hashtbl.create 17;;
 672   let count_terms = ref (-1);;
 673
 674   let share_csts out out_types name = function
 675     | Heq a ->
 676         let n = share_types out_types a in
 677         out "\nDefinition "; out name; out " := Cst (Heq "; out n; out ")."
 678     | Heps a ->
 679         let n = share_types out_types a in
 680         out "\nDefinition "; out name; out " := Cst (Heps "; out n; out ")."
 681     | Hand -> out "\nDefinition "; out name; out " := Cst Hand."
 682     | Hor -> out "\nDefinition "; out name; out " := Cst Hor."
 683     | Hnot -> out "\nDefinition "; out name; out " := Cst Hnot."
 684     | Himp -> out "\nDefinition "; out name; out " := Cst Himp."
 685     | Htrue -> out "\nDefinition "; out name; out " := Cst Htrue."
 686     | Hfalse -> out "\nDefinition "; out name; out " := Cst Hfalse."
 687     | Hforall a ->
 688         let n = share_types out_types a in
 689         out "\nDefinition "; out name; out " := Cst (Hforall "; out n; out ")."
 690     | Hexists a ->
 691         let n = share_types out_types a in
 692         out "\nDefinition "; out name; out " := Cst (Hexists "; out n; out ")."
 693
 694   let share_terms out out_types tm =
 695
 696     let rec share_terms tm =
 697       try Hashtbl.find the_terms tm with
 698         | Not_found ->
 699             incr count_terms;
 700             let name = THEORY_NAME^"_term_"^(string_of_int !count_terms) in
 701             (match tm with
 702                | Napp(t1,t2) ->
 703                    let n1 = share_terms t1 in
 704                    let n2 = share_terms t2 in
 705                    out "\nDefinition "; out name; out " := App "; out n1; out " "; out n2; out "."
 706                | Nabs(ty,t) ->
 707                    let n = share_terms t in
 708                    let ny = share_types out_types ty in
 709                    out "\nDefinition "; out name; out " := Abs "; out ny; out " "; out n; out "."
 710                | Nvar(i,ty) ->
 711                    let ny = share_types out_types ty in
 712                    out "\nDefinition "; out name; out " := Var "; print_names out i; out " "; out ny; out "."
 713                | Ndef(i,ty) ->
 714                    let ny = share_types out_types ty in
 715                    out "\nDefinition "; out name; out " := Def "; print_names out i; out " "; out ny; out "."
 716                | Ncst c -> share_csts out out_types name c
 717                | t -> out "\nDefinition "; out name; out " := "; print_term out t; out ".");
 718             Hashtbl.add the_terms tm name;
 719             name in
 720
 721     share_terms tm;;
 722
 723
 724   let export_proof out share_type share_term p =
 725
 726     let rec wp = function
 727       | Nprefl tm ->
 728           let tm2 = share_term tm in
 729           out "(Prefl "; out tm2; out ")"
 730       | Npbeta (n, ty, tm) ->
 731           let tm2 = share_term tm in
 732           let ty2 = share_type ty in
 733           out "(Pbeta "; print_names out n; out " "; out ty2; out " "; out tm2; out ")"
 734       | Npinstt(p,lambda) ->
 735           out "(Pinstt ";
 736           wp p;
 737           out " "; print_list out (fun (s, ty) ->
 738                                      let ty2 = share_type ty in
 739                                      out "("; print_names out s; out ", "; out ty2; out ")") "nil" "cons" lambda; out ")"
 740       | Npabs(p,x,ty) ->
 741           let ty2 = share_type ty in
 742           out "(Pabs ";
 743           wp p;
 744           out " "; print_names out x;
 745           out " "; out ty2; out ")"
 746       | Npdisch(p,tm) ->
 747           let tm2 = share_term tm in
 748           out "(Pdisch ";
 749           wp p;
 750           out " "; out tm2; out ")"
 751       | Nphyp tm ->
 752           let tm2 = share_term tm in
 753           out "(Phyp "; out tm2; out ")"
 754       | Npaxm(_, _) -> ()
 755       | Npdef(_, _, _) -> ()
 756       | Nptyintro(_, _, _, _, _) -> ()
 757       | Npspec(p,t) ->
 758           let t2 = share_term t in
 759           out "(Pspec ";
 760           wp p;
 761           out " "; out t2; out ")"
 762       | Npinst(p,theta) ->
 763           out "(Pinst ";
 764           wp p;
 765           out " "; print_list out (fun (s, ty, t) ->
 766                                      let t2 = share_term t in
 767                                      let ty2 = share_type ty in
 768                                      out "("; print_names out s; out ", "; out ty2; out ", "; out t2; out ")") "nil" "cons" theta; out ")"
 769       | Npgen(p,x,ty) ->
 770           let ty2 = share_type ty in
 771           out "(Pgen ";
 772           wp p;
 773           out " "; print_names out x; out " "; out ty2; out ")"
 774       | Npsym p ->
 775           out "(Psym ";
 776           wp p;
 777           out ")"
 778       |  Nptrans(p1,p2) ->
 779            out "(Ptrans ";
 780            wp p1;
 781            out " ";
 782            wp p2;
 783            out ")"
 784       | Npcomb(p1,p2) ->
 785           out "(Pcomb ";
 786           wp p1;
 787           out " ";
 788           wp p2;
 789           out ")"
 790       | Npeqmp(p1,p2) ->
 791           out "(Peqmp ";
 792           wp p1;
 793           out " ";
 794           wp p2;
 795           out ")"
 796       | Npexists(p,ex,w) ->
 797           let ex2 = share_term ex in
 798           let w2 = share_term w in
 799           out "(Pexists ";
 800           wp p;
 801           out " "; out ex2; out " "; out w2; out ")"
 802       | Npchoose(x,ty,p1,p2) ->
 803           let ty2 = share_type ty in
 804           out "(Pchoose "; print_names out x; out " "; out ty2; out " ";
 805           wp p1;
 806           out " ";
 807           wp p2;
 808           out ")"
 809       | Npconj(p1,p2) ->
 810           out "(Pconj ";
 811           wp p1;
 812           out " ";
 813           wp p2;
 814           out ")"
 815       | Npimpas(p1,p2) ->
 816           out "(Pimpas ";
 817           wp p1;
 818           out " ";
 819           wp p2;
 820           out ")"
 821       | Npconjunct1 p ->
 822           out "(Pconjunct1 ";
 823           wp p;
 824           out ")"
 825       |  Npconjunct2 p ->
 826            out "(Pconjunct2 ";
 827            wp p;
 828            out ")"
 829       | Npdisj1(p,tm) ->
 830           let tm2 = share_term tm in
 831           out "(Pdisj1 ";
 832           wp p;
 833           out " "; out tm2; out ")"
 834       | Npdisj2(p,tm) ->
 835           let tm2 = share_term tm in
 836           out "(Pdisj2 ";
 837           wp p;
 838           out " "; out tm2; out ")"
 839       | Npdisjcases(p1,p2,p3) ->
 840           out "(Pdisjcases ";
 841           wp p1;
 842           out " ";
 843           wp p2;
 844           out " ";
 845           wp p3;
 846           out ")"
 847       | Npnoti p ->
 848           out "(Pnoti ";
 849           wp p;
 850           out ")"
 851       | Npnote p ->
 852           out "(Pnote ";
 853           wp p;
 854           out ")"
 855       | Npcontr(p,tm) ->
 856           let tm2 = share_term tm in
 857           out "(Pcontr ";
 858           wp p;
 859           out " "; out tm2; out ")"
 860       | Nfact(thm) -> out "(Poracle "; out thm; out "_def)" in
 861
 862     wp p;;
 863
 864
 865   let export_ht out share_term h t thmname =
 866     out "\n\n\nDefinition "; out thmname; out "_h := ";
 867     (match h with
 868        | [] -> out "hyp_empty"
 869        | _ -> print_list out (fun tm ->
 870                                 let tm2 = share_term tm in
 871                                 out tm2) "nil" "cons" h);
 872     out ".\n\nDefinition "; out thmname; out "_t := ";
 873     let t2 = share_term t in
 874     out t2; out ".";;
 875
 876
 877   let export_lemma out share_type share_term p thmname =
 878     out "\n\nLemma "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname;
 879     out "_t.\nProof.\n  vm_cast_no_check (proof2deriv_correct "; export_proof out share_type share_term p; out ").\nQed.";;
 880
 881
 882   let export_lemma_def out tree thmname =
 883     out "\n\nLemma "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname;
 884     out "_t.\nProof.\n  vm_cast_no_check (proof2deriv_correct "; out tree; out ").\nQed.";;
 885
 886
 887   let export_sig out thmname =
 888     out "\n\nDefinition "; out thmname; out "_def := my_exist "; out thmname; out "_lemma.";;
 889
 890
 891   let export_def out thmname =
 892     out "\n\nParameter "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
 893
 894
 895   let export_tdef out thmname =
 896     out "\n\nParameter "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
 897
 898
 899   let export_axiom out thmname =
 900     out "\n\nAxiom "; out thmname; out "_lemma : deriv "; out thmname; out "_h "; out thmname; out "_t.";;
 901
 902
 903   (* Transforming a proof into a derivation *)
 904
 905   let rec opt_nth n l =
 906     match (n, l) with
 907       | 0, (x::_) -> Some x
 908       | 0, [] -> None
 909       | p, (_::l) -> opt_nth (p-1) l
 910       | _, _ -> None;;
 911
 912
 913   let type_cst = function
 914     | Heq a -> Narrow(a, Narrow(a, Nbool))
 915     | Heps a -> Narrow(Narrow(a, Nbool), a)
 916     | Hand -> Narrow(Nbool, Narrow(Nbool, Nbool))
 917     | Hor -> Narrow(Nbool, Narrow(Nbool, Nbool))
 918     | Hnot -> Narrow(Nbool, Nbool)
 919     | Himp -> Narrow(Nbool, Narrow(Nbool, Nbool))
 920     | Htrue -> Nbool
 921     | Hfalse -> Nbool
 922     | Hforall a -> Narrow(Narrow(a, Nbool), Nbool)
 923     | Hexists a -> Narrow(Narrow(a, Nbool), Nbool);;
 924
 925
 926   let rec infer g = function
 927     | Ndbr n -> opt_nth n g
 928     | Nvar (_, a) -> Some a
 929     | Ncst c -> Some (type_cst c)
 930     | Ndef (_, a) -> Some a
 931     | Napp (t1, t2) ->
 932         (match infer g t1, infer g t2 with
 933            | Some (Narrow (u1, u2)), Some v -> if u1 = v then Some u2 else None
 934            | _, _ -> None)
 935     | Nabs (a, u) ->
 936         (match infer (a::g) u with
 937            | Some b -> Some (Narrow (a, b))
 938            | None -> None);;
 939
 940
 941   let rec close_aux t x a i =
 942     match t with
 943       | Ndbr n -> Ndbr (if n < i then n else n+1)
 944       | Nvar (y, b) -> if ((x = y) && (a = b)) then Ndbr i else Nvar (y, b)
 945       | Napp (t1, t2) -> Napp (close_aux t1 x a i, close_aux t2 x a i)
 946       | Nabs (b, u) -> Nabs(b, close_aux u x a (i+1))
 947       | u -> u;;
 948
 949   let close t x a = close_aux t x a 0;;
 950
 951
 952   let rec subst_idt_type_aux x = function
 953     | [] -> Ntvar x
 954     | (y,a)::q -> if x = y then a else subst_idt_type_aux x q;;
 955
 956   let rec subst_idt_type t s =
 957     match t with
 958       | Ntvar x -> subst_idt_type_aux x s
 959       | Ntdef (a, l) -> Ntdef (a, subst_idt_list_type l s)
 960       | Narrow (a, b) -> Narrow (subst_idt_type a s, subst_idt_type b s)
 961       | u -> u
 962
 963   and subst_idt_list_type l s = List.map (fun t -> subst_idt_type t s) l;;
 964
 965   let rec subst_idt t s =
 966     match t with
 967       | Nvar (x, y)      -> Nvar (x, subst_idt_type y s)
 968       | Ncst (Heq a)     -> Ncst (Heq (subst_idt_type a s))
 969       | Ncst (Heps a)    -> Ncst (Heps (subst_idt_type a s))
 970       | Ncst (Hforall a) -> Ncst (Hforall (subst_idt_type a s))
 971       | Ncst (Hexists a) -> Ncst (Hexists(subst_idt_type a s))
 972       | Ndef (c, d)      -> Ndef (c, subst_idt_type d s)
 973       | Napp (t1, t2)    -> Napp (subst_idt t1 s, subst_idt t2 s)
 974       | Nabs (a, t)      -> Nabs (subst_idt_type a s, subst_idt t s)
 975       | u                -> u;;
 976
 977   let subst_idt_context g s = List.map (fun a -> subst_idt_type a s) g;;
 978
 979   let rec subst_idv_aux x y s =
 980       match s with
 981         | [] -> Nvar (x, y)
 982         | (z, t, u)::q -> if ((x = z) && (y = t)) then u else subst_idv_aux x y q;;
 983
 984   let rec subst_idv t s =
 985     match t with
 986       | Nvar (x, y) -> subst_idv_aux x y s
 987       | Napp (t1, t2) -> Napp (subst_idv t1 s, subst_idv t2 s)
 988       | Nabs (a, t) -> Nabs (a, subst_idv t s)
 989       | u -> u;;
 990
 991   let rec wf_substitution_idv = function
 992     | [] -> true
 993     | (_,y,t)::q ->
 994         match infer [] t with
 995           | Some z -> if (y = z) then wf_substitution_idv q else false
 996           | None -> false;;
 997
 998
 999   let rec is_not_free x y = function
1000     | Nvar (z, t) -> (x != z) or (not (y = t))
1001     | Napp (t1, t2) -> (is_not_free x y t1) && (is_not_free x y t2)
1002     | Nabs (_, u) -> is_not_free x y u
1003     | _ -> true;;
1004
1005
1006   let rec lift_term u i j =
1007     match u with
1008       | Ndbr n -> if n >= i then Ndbr (j + n) else Ndbr n
1009       | Napp (u1, u2) -> Napp (lift_term u1 i j, lift_term u2 i j)
1010       | Nabs (a, t) -> Nabs (a, lift_term t (i+1) j)
1011       | u -> u;;
1012
1013   let rec subst_db t n u =
1014     match t with
1015       | Ndbr i -> if i < n then Ndbr i else if i = n then u else Ndbr (i-1)
1016       | Napp (t1, t2) -> Napp (subst_db t1 n u, subst_db t2 n u)
1017       | Nabs (a, t) -> Nabs (a, subst_db t (n+1) (lift_term u 0 1))
1018       | u -> u;;
1019
1020   let nopen t u = subst_db t 0 u;;
1021
1022
1023   let heq a t u = Napp (Napp (Ncst (Heq a), t), u);;
1024   let hequiv t u = Napp (Napp (Ncst (Heq Nbool), t), u);;
1025   let himp t u = Napp (Napp (Ncst Himp, t), u);;
1026   let hand t u = Napp (Napp (Ncst Hand, t), u);;
1027   let hor t u = Napp (Napp (Ncst Hor, t), u);;
1028   let hnot t = Napp (Ncst Hnot, t);;
1029   let htrue = Ncst Htrue;;
1030   let hfalse = Ncst Hfalse;;
1031   let hforall a p = Napp (Ncst (Hforall a), Nabs (a, p));;
1032   let hexists a p = Napp (Ncst (Hexists a), Nabs (a, p));;
1033
1034
1035   let hyp_empty = [];;
1036
1037   let rec hyp_remove e = function
1038     | [] -> []
1039     | t::q -> if (e = t) then q else t::(hyp_remove e q);;
1040
1041   let rec hyp_add e = function
1042     | [] -> [e]
1043     | t::q -> if (e = t) then t::q else t::(hyp_add e q);;
1044
1045   let hyp_union l m = List.fold_left (fun n e -> hyp_add e n) m l;;
1046
1047   let hyp_map f l = List.fold_left (fun m e -> hyp_add (f e) m) [] l;;
1048
1049   let hyp_singl e = [e];;
1050
1051   let rec hyp_is_not_free x y = function
1052     | [] -> true
1053     | t::q -> (is_not_free x y t) && (hyp_is_not_free x y q);;
1054
1055   let hyp_subst_idt h s = hyp_map (fun t -> subst_idt t s) h;;
1056
1057   let hyp_subst_idv h s = hyp_map (fun t -> subst_idv t s) h;;
1058
1059
1060   let rec eq_type a b = match (a,b) with
1061     | Ntvar i, Ntvar j -> i = j
1062     | Nbool, Nbool -> true
1063     | Nnum, Nnum -> true
1064     | Narrow(a1, b1), Narrow(a2, b2) -> (eq_type a1 a2) && (eq_type b1 b2)
1065     | Ntdef(i,l), Ntdef(j,m) -> (i = j) && (eq_list_type l m)
1066     | _, _ -> false
1067
1068   and eq_list_type l m = match (l,m) with
1069     | [], [] -> true
1070     | t1::q1, t2::q2 -> (eq_type t1 t2) && (eq_list_type q1 q2)
1071     | _, _ -> false;;
1072
1073
1074   let eq_cst a b = match (a,b) with
1075     | Heq a, Heq b -> eq_type a b
1076     | Heps a, Heps b -> eq_type a b
1077     | Hand, Hand -> true
1078     | Hor, Hor -> true
1079     | Hnot, Hnot -> true
1080     | Himp, Himp -> true
1081     | Htrue, Htrue -> true
1082     | Hfalse, Hfalse -> true
1083     | Hforall a, Hforall b -> eq_type a b
1084     | Hexists a, Hexists b -> eq_type a b
1085     | _, _ -> false;;
1086
1087
1088   let rec eq_term a b = match (a,b) with
1089     | Ndbr i, Ndbr j -> i = j
1090     | Nvar(i,a), Nvar(j,b) -> (i = j) && (eq_type a b)
1091     | Ncst c, Ncst d -> eq_cst c d
1092     | Ndef(i,a), Ndef(j,b) -> (i = j) && (eq_type a b)
1093     | Napp(a1,b1), Napp(a2,b2) -> (eq_term a1 a2) && (eq_term b1 b2)
1094     | Nabs(t1,a1), Nabs(t2,a2) -> (eq_type t1 t2) && (eq_term a1 a2)
1095     | _, _ -> false;;
1096
1097
1098   let derivs = Hashtbl.create 17;;
1099
1100
1101   let rec proof2deriv = function
1102
1103     | Nprefl t ->
1104         (match infer [] t with
1105            | Some a -> Some (hyp_empty, heq a t t)
1106            | None -> (print_string "Nprefl\n"); None)
1107
1108     | Npbeta (x, y, t) ->
1109         (match infer [] t with
1110            | Some a -> Some (hyp_empty,
1111                              heq a (Napp (Nabs (y, close t x y), Nvar (x, y))) t)
1112            | None -> (print_string "Npbeta\n"); None)
1113
1114     | Npinstt (q, l) ->
1115         (match proof2deriv q with
1116            | Some (h,v) -> Some (hyp_subst_idt h l, subst_idt v l)
1117            | None -> (print_string "Npinstt\n"); None)
1118
1119     | Npabs (q, x, y) ->
1120         (match proof2deriv q with
1121            | Some (h, t) ->
1122                (match t with
1123                   | Napp (Napp (Ncst (Heq a), t1), t2) ->
1124                       if hyp_is_not_free x y h then
1125                         Some (h, heq (Narrow (y, a)) (Nabs (y, close t1 x y)) (Nabs (y, close t2 x y)))
1126                       else ((print_string "Npabs\n"); None)
1127                   | _ -> (print_string "Npabs\n"); None)
1128            | None -> (print_string "Npabs\n"); None)
1129
1130     | Npdisch (q, t) ->
1131         (match proof2deriv q, infer [] t with
1132            | Some (h, u), Some Nbool -> Some (hyp_remove t h, himp t u)
1133            | _, _ -> (print_string "Npdisch\n"); None)
1134
1135     | Nphyp t ->
1136         (match infer [] t with
1137            | Some Nbool -> Some (hyp_singl t, t)
1138            | _ -> (print_string "Nphyp\n"); None)
1139
1140     | Npspec (q, t) ->
1141         (match proof2deriv q, infer [] t with
1142            | Some (h, u), Some a ->
1143                (match u with
1144                   | Napp (Ncst (Hforall b), Nabs (c, v)) ->
1145                       if ((eq_type a b) && (eq_type b c)) then
1146                         Some (h, nopen v t)
1147                       else ((print_string "Npspec\n"); None)
1148                   | _ -> (print_string "Npspec\n"); None)
1149            | _, _ -> (print_string "Npspec\n"); None)
1150
1151     | Npinst (q, l) ->
1152         (match proof2deriv q, wf_substitution_idv l with
1153            | Some (h, v), true -> Some (hyp_subst_idv h l, subst_idv v l)
1154            | _, _ -> (print_string "Npinst\n"); None)
1155
1156     | Npgen (q, x, y) ->
1157         (match proof2deriv q with
1158            | Some (h, t) ->
1159                if hyp_is_not_free x y h then
1160                  Some (h, hforall y (close t x y))
1161                else ((print_string "Npgen\n"); None)
1162            | None -> (print_string "Npgen\n"); None)
1163
1164     | Npsym q ->
1165         (match proof2deriv q with
1166            | Some (h, t) ->
1167                (match t with
1168                   | Napp (Napp (Ncst (Heq a), u), v) -> Some (h, heq a v u)
1169                   | _ -> (print_string "Npsym\n"); None)
1170            | None -> (print_string "Npsym\n"); None)
1171
1172     | Nptrans (q1, q2) ->
1173         (match proof2deriv q1, proof2deriv q2 with
1174            | Some (h1, t1), Some (h2, t2) ->
1175                (match t1, t2 with
1176                   | Napp (Napp (Ncst (Heq a), u1), u2),
1177                     Napp (Napp (Ncst (Heq b), v2), v3) ->
1178                       if ((eq_type a b) && (eq_term u2 v2)) then
1179                         Some (hyp_union h1 h2, heq a u1 v3)
1180                       else ((print_string "Nptrans\n"); None)
1181                   | _, _ -> (print_string "Nptrans\n"); None)
1182            | _, _ -> (print_string "Nptrans\n"); None)
1183
1184     | Npcomb (q1, q2) ->
1185         (match proof2deriv q1, proof2deriv q2 with
1186            | Some (h1, t1), Some (h2, t2) ->
1187                (match t1, t2 with
1188                   | Napp (Napp (Ncst (Heq (Narrow (a, b))), f), g),
1189                     Napp (Napp (Ncst (Heq c), u), v) ->
1190                       if (eq_type a c) then
1191                         Some (hyp_union h1 h2, heq b (Napp (f, u)) (Napp (g, v)))
1192                       else ((print_string "Npcomb\n"); None)
1193                   | _, _ -> (print_string "Npcomb\n"); None)
1194            | _, _ -> (print_string "Npcomb\n"); None)
1195
1196     | Npeqmp (q1, q2) ->
1197         (match proof2deriv q1, proof2deriv q2 with
1198            | Some (h1, t1), Some (h2, t2) ->
1199                (match t1 with
1200                   | Napp (Napp (Ncst (Heq Nbool), a), b) ->
1201                       if (eq_term a t2) then
1202                         Some (hyp_union h1 h2, b)
1203                       else ((print_string "Npeqmp\n"); None)
1204                   | _ -> (print_string "Npeqmp\n"); None)
1205            | _, _ -> (print_string "Npeqmp\n"); None)
1206
1207     | Npexists (q, b, t) ->
1208         (match proof2deriv q, b, infer [] t with
1209            | Some (h, u), Nabs (bb, a), Some aa ->
1210                if ((eq_type aa bb) && (eq_term (nopen a t) u)) then
1211                  Some (h, hexists aa a)
1212                else ((print_string "Npexists\n"); None)
1213            | _, _, _ -> (print_string "Npexists\n"); None)
1214
1215     | Npchoose (v, aa, q1, q2) ->
1216         (match proof2deriv q1, proof2deriv q2 with
1217            | Some (h1, t), Some (h2, c) ->
1218                (match t with
1219                   | Napp (Ncst (Hexists bb), Nabs (cc, a)) ->
1220                       let s = hyp_remove (nopen a (Nvar (v, aa))) h2 in
1221                       if ((eq_type aa bb) && (eq_type bb cc) && (hyp_is_not_free v aa s) && (is_not_free v aa c)
1222                           && (is_not_free v aa a)) then
1223                         Some (hyp_union h1 s, c)
1224                       else ((print_string "Npchoose\n"); None)
1225                   | _ -> (print_string "Npchoose\n"); None)
1226            | _, _ -> (print_string "Npchoose\n"); None)
1227
1228     | Npconj (q1, q2) ->
1229         (match proof2deriv q1, proof2deriv q2 with
1230            | Some (h1, a), Some (h2, b) ->
1231                Some (hyp_union h1 h2, hand a b)
1232            | _, _ -> (print_string "Npconj\n"); None)
1233
1234     | Npconjunct1 q ->
1235         (match proof2deriv q with
1236            | Some (h, v) ->
1237                (match v with
1238                   | Napp (Napp (Ncst Hand, t), u) ->
1239                       Some (h, t)
1240                   | _ -> (print_string "Npconjunct1\n"); None)
1241            | _ -> (print_string "Npconjunct1\n"); None)
1242
1243     | Npconjunct2 q ->
1244         (match proof2deriv q with
1245            | Some (h, v) ->
1246                (match v with
1247                   | Napp (Napp (Ncst Hand, t), u) ->
1248                       Some (h, u)
1249                   | _ -> (print_string "Npconjunct2\n"); None)
1250            | _ -> (print_string "Npconjunct2\n"); None)
1251
1252     | Npdisj1 (q, b) ->
1253         (match proof2deriv q, infer [] b with
1254            | Some (h, a), Some Nbool -> Some (h, hor a b)
1255            | _, _ -> (print_string "Npdisj1\n"); None)
1256
1257     | Npdisj2 (q, a) ->
1258         (match proof2deriv q, infer [] a with
1259            | Some (h, b), Some Nbool -> Some (h, hor a b)
1260            | _, _ -> (print_string "Npdisj1\n"); None)
1261
1262     | Npdisjcases (q1, q2, q3) ->
1263         (match proof2deriv q1, proof2deriv q2, proof2deriv q3 with
1264            | Some (h1, t), Some (h2, c1), Some (h3, c2) ->
1265                (match t with
1266                   | Napp (Napp (Ncst Hor, a), b) ->
1267                       if (eq_term c1 c2) then
1268                         Some (hyp_union h1 (hyp_union (hyp_remove a h2) (hyp_remove b h3)), c1)
1269                       else ((print_string "Npdisjcases\n"); None)
1270                   | _ -> (print_string "Npdisjcases\n"); None)
1271            | _, _, _ -> (print_string "Npisjcases\n"); None)
1272
1273     | Npnoti q ->
1274         (match proof2deriv q with
1275            | Some (h, t) ->
1276                (match t with
1277                   | Napp (Napp (Ncst Himp, a), Ncst Hfalse) -> Some (h, hnot a)
1278                   | _ -> (print_string "Npnoti\n"); None)
1279            | _ -> (print_string "Npnoti\n"); None)
1280
1281     | Npnote q ->
1282         (match proof2deriv q with
1283            | Some (h, t) ->
1284                (match t with
1285                   | Napp (Ncst Hnot, a) -> Some (h, himp a hfalse)
1286                   | _ -> (print_string "Npnote\n"); None)
1287            | _ -> (print_string "Npnote\n"); None)
1288
1289     | Npcontr (q, a) ->
1290         (match proof2deriv q, infer [] a with
1291            | Some (h, t), Some Nbool ->
1292                (match t with
1293                   | Ncst Hfalse -> Some (hyp_remove (hnot a) h, a)
1294                   | _ -> (print_string "Npcontr\n"); None)
1295            | _, _ -> (print_string "Npcontr\n"); None)
1296
1297     | Npimpas (q1, q2) ->
1298         (match proof2deriv q1, proof2deriv q2 with
1299            | Some (h1, t), Some (h2, u) ->
1300                (match t, u with
1301                   | Napp (Napp (Ncst Himp, a1), b1),
1302                     Napp (Napp (Ncst Himp, b2), a2) ->
1303                       if ((eq_term a1 a2) && (eq_term b1 b2)) then
1304                         Some (hyp_union h1 h2, hequiv b1 a1)
1305                       else ((print_string ("Npimpas1; 1: "^(string_of_bool (eq_term a1 a2))^"; 2: "^(string_of_bool (eq_term b1 b2))^"\n"));
1306                             let out = print_string in
1307                             print_term out a1; out "\n"; print_term out a2; out "\n"; print_term out b1; out "\n"; print_term out b2; out "\n"; None)
1308                   | _, _ -> (print_string "Npimpas2\n"); None)
1309            | _, _ -> (print_string "Npimpas3\n"); None)
1310
1311     | Nfact thm ->
1312         (try Some (Hashtbl.find derivs thm) with
1313            | Not_found -> (print_string ("Nfact "^thm^"\n")); None)
1314
1315     | Npdef (i, a, t) -> Some (hyp_empty, heq a (Ndef (i, a)) t)
1316
1317     | Npaxm (_, t) -> Some (hyp_empty, t)
1318
1319     | Nptyintro (rty, aty, mk_name, dest_name, p) ->
1320
1321         let mk_type = Narrow(rty, aty) in
1322         let dest_type = Narrow(aty, rty) in
1323
1324         let a_name = make_idV "a" aty in
1325         let a = Nvar(a_name, aty) in
1326         let r_name = make_idV "r" rty in
1327         let r = Nvar(r_name, rty) in
1328
1329         Some (hyp_empty, hand (heq aty (Napp (Ndef (mk_name, mk_type), Napp (Ndef (dest_name, dest_type), a))) a)
1330                 (hequiv (Napp (p, r)) (heq rty (Napp (Ndef (dest_name, dest_type), Napp (Ndef (mk_name, mk_type), r))) r)));;
1331
1332
1333   (* Dealing with dependencies *)
1334
1335   let rec make_dependencies_aux dep_graph proof_of_thm = function
1336     | [] -> ()
1337     | (thmname, p, c_opt)::il ->
1338
1339         incr total;
1340
1341         let wdi thm =
1342           Depgraph.Dep.add_dep dep_graph thm thmname;
1343           Nfact thm in
1344
1345         let write_proof p il =
1346
1347           let rec share_info_of p il =
1348             match (disk_info_of p) with
1349               | Some (thyname,thmname) -> Some(thyname,thmname,il)
1350               | None ->
1351                   if do_share p then
1352                     let name = THEORY_NAME^"_"^(get_iname ()) in
1353                     set_disk_info_of p THEORY_NAME name;
1354                     Depgraph.Dep.add_thm dep_graph name;
1355                     Some(THEORY_NAME,name,(name,p,None)::il)
1356                   else
1357                     None
1358
1359           and wp' il = function
1360             | Prefl tm -> Nprefl (term2nterm tm), il
1361             | Pbeta(x, ty, tm) ->
1362                 let typ = hol_type2ntype ty in
1363                 Npbeta(make_idV x typ , typ, term2nterm tm), il
1364             | Pinstt(p,lambda) ->
1365                 let p', res = wp il p in
1366                 Npinstt(p', List.map (
1367                           fun (s,ty) -> (make_idT s, hol_type2ntype ty)
1368                         ) lambda), res
1369             | Pabs(p,x,ty) ->
1370                 let p', res = wp il p in
1371                 let typ = hol_type2ntype ty in
1372                 Npabs(p',make_idV x typ,typ), res
1373             | Pdisch(p,tm) ->
1374                 let p', res = wp il p in
1375                 Npdisch(p', term2nterm tm), res
1376             | Phyp tm -> Nphyp (term2nterm tm), il
1377             | Paxm(th,tm) -> Npaxm(th, term2nterm tm), il
1378             | Pdef(name,ty,tm) ->
1379                 let typ = hol_type2ntype ty in
1380                 Npdef(make_defV name typ true, typ, term2nterm tm), il
1381             | Ptyintro(rty2, tyname, tyvars, absname, repname, pt) ->
1382                 let rty = hol_type2ntype rty2 in
1383                 let new_name = make_defT tyname in
1384
1385                 let ntyvars = List.map hol_type2ntype tyvars in
1386                 let aty = Ntdef(new_name, ntyvars) in
1387
1388                 let mk_name = make_defV absname (Narrow(rty, aty)) false in
1389                 let dest_name = make_defV repname (Narrow(aty, rty)) false in
1390
1391                 Nptyintro(rty, aty, mk_name, dest_name, term2nterm pt), il
1392             | Pspec(p,t) ->
1393                 let p', res = wp il p in
1394                 Npspec(p', term2nterm t), res
1395             | Pinst(p,theta) ->
1396                 let p', res = wp il p in
1397                 Npinst(p', List.map (
1398                          fun (s,ty,te) ->
1399                            let typ = hol_type2ntype ty in
1400                            (make_idV s typ, typ, term2nterm te)
1401                        ) theta), res
1402             | Pgen(p,x,ty) ->
1403                 let p', res = wp il p in
1404                 let typ = hol_type2ntype ty in
1405                 Npgen(p', make_idV x typ, typ), res
1406             | Psym p ->
1407                 let p', res = wp il p in
1408                 Npsym p', res
1409             | Ptrans(p1,p2) ->
1410                 let p1', il' = wp il p1 in
1411                 let p2', res = wp il' p2 in
1412                 Nptrans(p1', p2'), res
1413             | Pcomb(p1,p2) ->
1414                 let p1', il' = wp il p1 in
1415                 let p2', res = wp il' p2 in
1416                 Npcomb(p1', p2'), res
1417             | Peqmp(p1,p2) ->
1418                 let p1', il' = wp il p1 in
1419                 let p2', res = wp il' p2 in
1420                 Npeqmp(p1', p2'), res
1421             | Pexists(p,ex,w) ->
1422                 let p', res = wp il p in
1423                 Npexists(p', term2nterm ex, term2nterm w), res
1424             | Pchoose(x,ty,p1,p2) ->
1425                 let p1', il' = wp il p1 in
1426                 let p2', res = wp il' p2 in
1427                 let typ = hol_type2ntype ty in
1428                 Npchoose(make_idV x typ, typ, p1', p2'), res
1429             | Pconj(p1,p2) ->
1430                 let p1', il' = wp il p1 in
1431                 let p2', res = wp il' p2 in
1432                 Npconj(p1', p2'), res
1433             | Pimpas(p1,p2) ->
1434                 let p1', il' = wp il p1 in
1435                 let p2', res = wp il' p2 in
1436                 Npimpas(p1', p2'), res
1437             | Pconjunct1 p ->
1438                 let p', res = wp il p in
1439                 Npconjunct1 p', res
1440             |  Pconjunct2 p ->
1441                  let p', res = wp il p in
1442                  Npconjunct2 p', res
1443             | Pdisj1(p,tm) ->
1444                 let p', res = wp il p in
1445                 Npdisj1(p', term2nterm tm), res
1446             | Pdisj2(p,tm) ->
1447                 let p', res = wp il p in
1448                 Npdisj2(p', term2nterm tm), res
1449             | Pdisjcases(p1,p2,p3) ->
1450                 let p1', il' = wp il p1 in
1451                 let p2', il'' = wp il' p2 in
1452                 let p3', res = wp il'' p3 in
1453                 Npdisjcases(p1', p2', p3'), res
1454             | Pnoti p ->
1455                 let p', res = wp il p in
1456                 Npnoti p', res
1457             | Pnote p ->
1458                 let p', res = wp il p in
1459                 Npnote p', res
1460             | Pcontr(p,tm) ->
1461                 let p', res = wp il p in
1462                 Npcontr(p', term2nterm tm), res
1463
1464           and wp il p =
1465             match share_info_of p il with
1466               | Some(_, thmname, il') -> wdi thmname, il'
1467               | None -> wp' il (content_of p) in
1468
1469           match disk_info_of p with
1470             | Some(_, thmname') -> if thmname' = thmname then wp' il (content_of p) else (wdi thmname', il)
1471             | None -> wp' il (content_of p) in
1472
1473         let p', il = write_proof p il in
1474         set_disk_info_of p THEORY_NAME thmname;
1475         Hashtbl.add proof_of_thm thmname p';
1476         make_dependencies_aux dep_graph proof_of_thm il;;
1477
1478
1479   let make_dependencies out out_share out_sharet new_file count_thms path ((thmname, pr, _) as p) =
1480
1481     let dep_graph = Depgraph.Dep.create () in
1482     let proof_of_thm = Hashtbl.create (references pr) in
1483     Depgraph.Dep.add_thm dep_graph thmname;
1484
1485     make_dependencies_aux dep_graph proof_of_thm [p];
1486
1487     let share_type ty = share_types out_sharet ty in
1488     let share_term ty = share_terms out_share out_sharet ty in
1489
1490
1491     if thmname = (THEORY_NAME^"_DEF_T") then (
1492       match content_of pr with
1493         | Pdef (_, _, t) ->
1494             let tm = hequiv htrue (term2nterm t) in
1495             Hashtbl.add derivs thmname (hyp_empty, tm);
1496             export_ht out share_term hyp_empty tm thmname;
1497             export_lemma_def out "DEF_T" thmname;
1498             export_sig out thmname
1499         | _ -> ()
1500     ) else if thmname = (THEORY_NAME^"_DEF__slash__backslash_") then (
1501       match content_of pr with
1502         | Pdef (_, _, t) ->
1503             let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Hand) (term2nterm t) in
1504             Hashtbl.add derivs thmname (hyp_empty, tm);
1505             export_ht out share_term hyp_empty tm thmname;
1506             export_lemma_def out "DEF_AND" thmname;
1507             export_sig out thmname
1508         | _ -> ()
1509     ) else if thmname = (THEORY_NAME^"_DEF__equal__equal__greaterthan_") then (
1510       match content_of pr with
1511         | Pdef (_, _, t) ->
1512             let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Himp) (term2nterm t) in
1513             Hashtbl.add derivs thmname (hyp_empty, tm);
1514             export_ht out share_term hyp_empty tm thmname;
1515             export_lemma_def out "DEF_IMP" thmname;
1516             export_sig out thmname
1517         | _ -> ()
1518     ) else if thmname = (THEORY_NAME^"_DEF__exclamationmark_") then (
1519       match content_of pr with
1520         | Pdef (_, a, t) ->
1521             let a2 = hol_type2ntype a in
1522             (match a2 with
1523                | Narrow (Narrow (b, _), _) ->
1524                    let tm = heq a2 (Ncst (Hforall b)) (term2nterm t) in
1525                    Hashtbl.add derivs thmname (hyp_empty, tm);
1526                    export_ht out share_term hyp_empty tm thmname;
1527                    export_lemma_def out "DEF_FORALL" thmname;
1528                    export_sig out thmname
1529                | _ -> ())
1530         | _ -> ()
1531     ) else if thmname = (THEORY_NAME^"_DEF__questionmark_") then (
1532       match content_of pr with
1533         | Pdef (_, a, t) ->
1534             let a2 = hol_type2ntype a in
1535             (match a2 with
1536                | Narrow (Narrow (b, _), _) ->
1537                    let tm = heq a2 (Ncst (Hexists b)) (term2nterm t) in
1538                    Hashtbl.add derivs thmname (hyp_empty, tm);
1539                    export_ht out share_term hyp_empty tm thmname;
1540                    export_lemma_def out "DEF_EXISTS" thmname;
1541                    export_sig out thmname
1542                | _ -> ())
1543         | _ -> ()
1544     ) else if thmname = (THEORY_NAME^"_DEF__backslash__slash_") then (
1545       match content_of pr with
1546         | Pdef (_, _, t) ->
1547             let tm = heq (Narrow (Nbool, Narrow (Nbool, Nbool))) (Ncst Hor) (term2nterm t) in
1548             Hashtbl.add derivs thmname (hyp_empty, tm);
1549             export_ht out share_term hyp_empty tm thmname;
1550             export_lemma_def out "DEF_OR" thmname;
1551             export_sig out thmname
1552         | _ -> ()
1553     ) else if thmname = (THEORY_NAME^"_DEF_F") then (
1554       match content_of pr with
1555         | Pdef (_, _, t) ->
1556             let tm = hequiv (Ncst Hfalse) (term2nterm t) in
1557             Hashtbl.add derivs thmname (hyp_empty, tm);
1558             export_ht out share_term hyp_empty tm thmname;
1559             export_lemma_def out "DEF_F" thmname;
1560             export_sig out thmname
1561         | _ -> ()
1562     ) else if thmname = (THEORY_NAME^"_DEF__tilde_") then (
1563       match content_of pr with
1564         | Pdef(_, _, t) ->
1565             let tm = heq (Narrow (Nbool, Nbool)) (Ncst Hnot) (term2nterm t) in
1566             Hashtbl.add derivs thmname (hyp_empty, tm);
1567             export_ht out share_term hyp_empty tm thmname;
1568             export_lemma_def out "DEF_NOT" thmname;
1569             export_sig out thmname
1570         | _ -> ()
1571     ) else if thmname = (THEORY_NAME^"_DEF__FALSITY_") then (
1572       let tm = heq Nbool (Ncst Hfalse) (Ncst Hfalse) in
1573       Hashtbl.add derivs thmname (hyp_empty, tm);
1574       export_ht out share_term hyp_empty tm thmname;
1575       export_lemma_def out "(Prefl (Cst Hfalse))" thmname;
1576       export_sig out thmname
1577     ) else if thmname = (THEORY_NAME^"_ax__1") then (
1578       match content_of pr with
1579         | Paxm (_, tm) ->
1580             let tm2 = term2nterm tm in
1581             Hashtbl.add derivs thmname (hyp_empty, tm2);
1582             export_ht out share_term hyp_empty tm2 thmname;
1583             export_lemma_def out "ETA_AX" thmname;
1584             export_sig out thmname
1585         | _ -> ()
1586     ) else if thmname = (THEORY_NAME^"_ax__2") then (
1587       match content_of pr with
1588         | Paxm (_, tm) ->
1589             let tm2 = term2nterm tm in
1590             Hashtbl.add derivs thmname (hyp_empty, tm2);
1591             export_ht out share_term hyp_empty tm2 thmname;
1592             export_lemma_def out "SELECT_AX" thmname;
1593             export_sig out thmname
1594         | _ -> ()
1595
1596     ) else (
1597
1598       Depgraph.Dep_top.iter_top (
1599         fun thm ->
1600           incr count_thms;
1601           if !count_thms = 1000 then (count_thms := 0; new_file ());
1602           (try
1603              let p = Hashtbl.find proof_of_thm thm in
1604              (match proof2deriv p with
1605                 | Some (h, t) ->
1606                     Hashtbl.add derivs thm (h, t);
1607                     export_ht out share_term h t thm;
1608                     (match p with
1609                        | Npdef _ -> export_def out thm
1610                        | Nptyintro _ -> export_tdef out thm
1611                        | Npaxm _ -> export_axiom out thm
1612                        | _ -> export_lemma out share_type share_term p thm);
1613                     export_sig out thm
1614                 | None -> failwith ("Erreur make_dependencies "^thm^" de "^thmname^": no derivation associated to the proof\n"))
1615            with | Not_found -> failwith ("Erreur make_dependencies "^thm^": proof_of_thm not found\n"));
1616       ) dep_graph
1617     );
1618 ;;
1619
1620
1621   let the_proof_database = ref ([]:(string*proof*(term option)) list);;
1622
1623   Random.self_init;;
1624
1625   let rec search_proof_name n db =
1626     match db with [] -> n | ((m, _, _)::db') -> if n=m then n^"_"^(string_of_int (Random.int 1073741823)) else search_proof_name n db'
1627
1628   let save_proof name p c_opt =
1629     let name' = search_proof_name name (!the_proof_database) in
1630     the_proof_database := (name', p, c_opt)::(!the_proof_database);;
1631
1632   let proof_database () = !the_proof_database;;
1633
1634
1635   (* Utilities to define Coq interpretation functions *)
1636
1637   let ut = Hashtbl.create 17;;
1638
1639   let ask_ut () =
1640     try (
1641       let filein = Pervasives.open_in "interpretation.txt" in
1642       let line = ref 0 in
1643
1644       try
1645         while true do
1646           incr line;
1647           let s1 = input_line filein in
1648           incr line;
1649           let s2 = input_line filein in
1650           Hashtbl.add ut s1 s2
1651         done
1652       with
1653         | End_of_file -> close_in filein
1654         | _ -> failwith ("Error line "^(string_of_int !line)^".")
1655     ) with | Sys_error _ -> ()
1656   ;;
1657
1658   let tc_regexp = Str.regexp "\?[0-9]*";;
1659
1660   let make_tc_parameter out x n =
1661     if Str.string_match tc_regexp x 0 then (
1662       let i = Str.match_end () in
1663       if i <> String.length x then (
1664         out "\nParameter "; out THEORY_NAME; out "_idT_"; out (mfc x); out " : Type.\nParameter "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x);
1665         out " : "; out THEORY_NAME; out "_idT_"; out (mfc x); out "."
1666       )
1667     ) else (
1668       out "\nParameter "; out THEORY_NAME; out "_idT_"; out (mfc x); out " : Type.\nParameter "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x);
1669       out " : "; out THEORY_NAME; out "_idT_"; out (mfc x); out "."
1670     );;
1671
1672   let make_tc_list out x n =
1673     if Str.string_match tc_regexp x 0 then (
1674       let i = Str.match_end () in
1675       if i <> String.length x then (
1676         out "\n("; out (string_of_int n); out ", mkTT "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x); out ")::"
1677       )
1678     ) else (
1679       out "\n("; out (string_of_int n); out ", mkTT "; out THEORY_NAME; out "_idT_inhab_"; out (mfc x); out ")::"
1680     );;
1681
1682
1683   let defT_ut = Hashtbl.create 17;;
1684
1685   let make_tdt_parameter out x _ =
1686     try (
1687       let y = Hashtbl.find ut x in
1688       Hashtbl.add defT_ut x y
1689     ) with | Not_found -> (
1690       out "\nParameter "; out THEORY_NAME; out "_defT_"; out (mfc x); out " : Type.";
1691       out "\nParameter "; out THEORY_NAME; out "_defT_inhab_"; out (mfc x); out " : "; out THEORY_NAME; out "_defT_"; out (mfc x); out ".\n";
1692       Hashtbl.add defT_ut x ("fun _ => mkTT "^THEORY_NAME^"_defT_inhab_"^(mfc x))
1693     );;
1694
1695   let make_tdt_list out x n =
1696     try (
1697       let s = Hashtbl.find defT_ut x in
1698       out "\n("; out (string_of_int n); out ", "; out s; out ")::";
1699     ) with | Not_found -> (
1700       out "\n("; out (string_of_int n); out ", fun _ => mkTT tt)::"
1701     );;
1702
1703
1704   let se_regexp = Str.regexp "_[0-9]*";;
1705
1706   let make_se_parameter out x (_,ty) =
1707     if Str.string_match se_regexp x 0 then (
1708       let i = Str.match_end () in
1709       if i <> String.length x then (
1710         out "\nParameter "; out THEORY_NAME; out "_idV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1711       )
1712     ) else (
1713       out "\nParameter "; out THEORY_NAME; out "_idV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1714     );;
1715
1716   let make_se_list out x (n,ty) =
1717     if Str.string_match se_regexp x 0 then (
1718       let i = Str.match_end () in
1719       if i <> String.length x then (
1720         out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_idV_"; out (mfc x); out ")::"
1721       )
1722     ) else (
1723       out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_idV_"; out (mfc x); out ")::"
1724     );;
1725
1726
1727   let defV_ut = Hashtbl.create 17;;
1728
1729   let make_sdt_parameter out x (_,ty,_) =
1730     if ((x <> "T") && (x <> "/\\") && (x <> "==>") && (x <> "!") && (x <> "?") && (x <> "\\/") && (x <> "F") && (x <> "~") && (x <> "_FALSITY_")) then (
1731       try (
1732         let y = Hashtbl.find ut x in
1733         Hashtbl.add defV_ut x y
1734       ) with | Not_found -> (
1735         out "\nParameter "; out THEORY_NAME; out "_defV_"; out (mfc x); out " : tr_type tc tdt "; print_type out ty; out "."
1736       )
1737     );;
1738
1739   let make_sdt_list out x (n,ty,_) =
1740     try (
1741       let s = Hashtbl.find defV_ut x in
1742       out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " ("; out s; out "))::"
1743     ) with | Not_found -> (
1744       if ((x <> "T") && (x <> "/\\") && (x <> "==>") && (x <> "!") && (x <> "?") && (x <> "\\/") && (x <> "F") && (x <> "~") && (x <> "_FALSITY_")) then (
1745         out "\n("; print_names out n; out ", existT (fun (t: type) => tr_type tc tdt t) "; print_type out ty; out " "; out THEORY_NAME; out "_defV_"; out (mfc x); out ")::"
1746       )
1747     );;
1748
1749
1750   (* Main function: list of proofs exportation *)
1751
1752   let export_list thmname_list =
1753
1754     total := 0;
1755
1756     let path = ensure_export_directory THEORY_NAME in
1757
1758
1759     let rec proof_of_thm acc acc2 = function
1760       | [] -> acc, acc2
1761       | (s,p,c)::q ->
1762           if List.mem s thmname_list then
1763             proof_of_thm ((THEORY_NAME^"_"^(mfc s), reset_disk_info_of1 p, c)::acc) (acc2+1) q
1764           else match content_of p with
1765             | Paxm _ | Pdef _ | Ptyintro _ -> proof_of_thm ((THEORY_NAME^"_"^(mfc s), reset_disk_info_of1 p, c)::acc) (acc2+1) q
1766             | _ -> proof_of_thm acc acc2 q in
1767
1768     let l, total_thms = proof_of_thm [] 0 (proof_database ()) in
1769
1770
1771     let count_thms = ref 0 in
1772     let count_files = ref 1 in
1773
1774     (* Main file *)
1775
1776     let file = ref (open_out (Filename.concat path (THEORY_NAME^"_1.v"))) in
1777     let count_file = ref 0 in
1778     let out s = (output_string !file s; incr count_file; if !count_file = 1000 then (count_file := 0; flush !file)) in
1779     out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Export List NArith.\nRequire Export hol deriv proof.\n\n";
1780
1781     (* Temporary file *)
1782
1783     let (file_temp_name, file_temp_aux) = Filename.open_temp_file (THEORY_NAME^"_") ".v" in
1784     let file_temp = ref file_temp_aux in
1785     let count_file_temp = ref 0 in
1786     let out_temp s = (output_string !file_temp s; incr count_file_temp; if !count_file_temp = 1000 then (count_file_temp := 0; flush !file_temp)) in
1787
1788
1789     let move_temp () =
1790       (try
1791          close_out !file_temp
1792        with | Sys_error s -> raise (Sys_error ("move_temp1: "^s)));
1793
1794       (try
1795          let buf = Pervasives.open_in file_temp_name in
1796          (try
1797             while true do
1798               out "\n";
1799               let l = input_line buf in
1800               out l
1801             done
1802           with | End_of_file -> close_in buf)
1803        with | Sys_error s -> raise (Sys_error ("move_temp3: "^s))) in
1804
1805
1806     (* New file *)
1807
1808     let new_file () =
1809
1810       move_temp ();
1811       file_temp := open_out file_temp_name;
1812
1813       incr count_files;
1814       close_out !file;
1815       file := open_out (Filename.concat path (THEORY_NAME^"_"^(string_of_int !count_files)^".v"));
1816       out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Export "; out THEORY_NAME; out "_"; out (string_of_int (!count_files-1)); out ".\n\n" in
1817
1818
1819     (* Coq files generation *)
1820
1821     let date1 = Unix.time () in
1822     List.iter (make_dependencies out_temp out out new_file count_thms path) l;
1823     let date2 = Unix.time () in
1824
1825
1826     move_temp (); close_out !file;
1827
1828
1829     (* Makefile *)
1830
1831     let make = open_out (Filename.concat path "Makefile") in
1832     let out = output_string make in
1833     out "# This file has been automatically generated from HOL-Light source files.\n\nCOQ=ssrcoq\nFLAGS=-dont-load-proofs -dump-glob /dev/null -compile\n\nSRC=";
1834     for i = 1 to !count_files do
1835       out " "; out THEORY_NAME; out "_"; out (string_of_int i); out ".v";
1836     done;
1837     out "\nOBJ=$(SRC:.v=.vo)\nGLOB=$(SRC:.v=.glob)\n\n\nall: $(OBJ)\n\n\n%.vo: %.v\n\t$(COQ) $(FLAGS) $(^:.v=)\n\n\nclean:\n\trm -f $(OBJ) $(GLOB) *~";
1838     close_out make;
1839
1840
1841     (* Interpretation *)
1842
1843     let interp = open_out (Filename.concat path "interpretation.v") in
1844     let out = output_string interp in
1845     out "(*** This file has been automatically generated from HOL-Light source files. ***)\n\nRequire Import ssreflect eqtype ssrnat ssrbool.\nRequire Import List NArith ZArith.ZOdiv_def.\nRequire Import hol cast typing translation axioms.\n\nOpen Local Scope positive_scope.\n\n";
1846
1847     ask_ut ();
1848
1849     (* tc *)
1850     Hashtbl.iter (make_tc_parameter out) idT;
1851     out "\n\nDefinition tc_list :=";
1852     Hashtbl.iter (make_tc_list out) idT;
1853     out "\nnil.\n\nDefinition tc := list_tc2tc tc_list.\n\n";
1854
1855     (* tdt *)
1856     Hashtbl.iter (make_tdt_parameter out) defT;
1857     out "\n\nDefinition tdt_list : list_tdt :=";
1858     Hashtbl.iter (make_tdt_list out) defT;
1859     out "\nnil.\n\nDefinition tdt := list_tdt2tdt tdt_list.\n\n";
1860
1861     (* se *)
1862     Hashtbl.iter (make_se_parameter out) idV;
1863     out "\n\nDefinition se_list :=";
1864     Hashtbl.iter (make_se_list out) idV;
1865     out "\nnil.\n\nDefinition se := list_se2se se_list.\n\n";
1866
1867     (* sdt *)
1868     Hashtbl.iter (make_sdt_parameter out) defV;
1869     out "\n\nDefinition sdt_list :=";
1870     Hashtbl.iter (make_sdt_list out) defV;
1871     out "\nnil.\n\nDefinition sdt := list_sdt2sdt sdt_list.";
1872
1873     close_out interp;
1874
1875
1876     print_string "Generated "; print_int !total; print_string " facts for "; print_int total_thms; print_string " theorems.\n";
1877     print_string "Exportation duration: "; print_float (date2 -. date1); print_string "s.\n"
1878   ;;
1879
1880
1881   (* Main function: all proofs exportation *)
1882
1883   let export_saved_proofs () = export_list (List.map (fun (s,_,_) -> s) (proof_database ()));;
1884
1885
1886   (* Main function: one proof exportation *)
1887
1888   let export_one_proof name = export_list [name];;
1889
1890
1891 end;;
1892
1893
1894 include Proofobjects;;