V8.8 (#42)

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Towards 8.8

* Organization structures

* 8.8 ok with standard coq

2 files changed, 177 insertions, 109 deletions

diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index dbf3d62..13beb9d 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -14,9 +14,80 @@ open Entries
 open Coqlib
 
 
+(* Constr generation and manipulation *)
+type id = Names.id
+let mkId = Names.id_of_string
+
+
+type name = Names.name
+let name_of_id i = Names.Name i
+let mkName s =
+  let id = mkId s in
+  name_of_id id
+let string_of_name = function
+    Names.Name id -> Names.string_of_id id
+  | _ -> failwith "unnamed rel"
+
+
+type constr = Term.constr
+type types = Term.types
+let eq_constr = Term.eq_constr
+let hash_constr = Term.hash_constr
+let mkProp = Term.mkProp
+let mkConst = Constr.mkConst
+let mkVar = Term.mkVar
+let mkRel = Term.mkRel
+let isRel = Term.isRel
+let destRel = Term.destRel
+let lift = Term.lift
+let mkApp = Term.mkApp
+let decompose_app = Term.decompose_app
+let mkLambda = Term.mkLambda
+let mkProd = Term.mkProd
+let mkLetIn = Term.mkLetIn
+
+let pr_constr_env = Printer.pr_constr_env
+let pr_constr = Printer.pr_constr
+
+let mkUConst c =
+  { const_entry_body = c;
+    const_entry_type = None;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+let mkTConst c _ ty =
+  { const_entry_body = c;
+    const_entry_type = Some ty;
+    const_entry_secctx = None;
+    const_entry_opaque = false;
+    const_entry_inline_code = false}
+
+(* TODO : Set -> Type *)
+let declare_new_type t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force Term.mkSet) [] false None (dummy_loc, t);
+  Term.mkVar t
+
+let declare_new_variable v constr_t =
+  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
+  Term.mkVar v
+
+let declare_constant n c =
+  Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
 
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
+type cast_kind = Term.cast_kind
+let vmcast = Term.VMcast
+let mkCast = Term.mkCast
+
+
+(* EConstr *)
+type econstr = Term.constr
+let econstr_of_constr e = e
+
+
+(* Modules *)
+let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 
 (* Int63 *)
@@ -64,58 +135,24 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
   mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace)
 
 
-(* Differences between the two versions of Coq *)
-type names_id_t = Names.identifier
-
-let dummy_loc = Pp.dummy_loc
-
-let mkUConst c =
-  { const_entry_body = c;
-    const_entry_type = None;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-let mkTConst c _ ty =
-  { const_entry_body = c;
-    const_entry_type = Some ty;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-let error = Errors.error
-
-let coqtype = lazy Term.mkSet
-
-let declare_new_type t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) (Lazy.force coqtype) [] false None (dummy_loc, t);
-  Term.mkVar t
-
-let declare_new_variable v constr_t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
-  Term.mkVar v
-
-let extern_constr = Constrextern.extern_constr true Environ.empty_env
-
-let vernacentries_interp expr =
-  Vernacentries.interp (Vernacexpr.VernacCheckMayEval (Some (Glob_term.CbvVm None), None, expr))
-
-let pr_constr_env = Printer.pr_constr_env
+(* Micromega *)
+module Micromega_plugin_Certificate = Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega
+module Micromega_plugin_Micromega = Micromega
+module Micromega_plugin_Mutils = Mutils
 
-let lift = Term.lift
+let micromega_coq_proofTerm =
+  Coq_micromega.M.coq_proofTerm
 
-let destruct_rel_decl (n, _, t) = n, t
+let micromega_dump_proof_term p =
+  Coq_micromega.dump_proof_term p
 
-let interp_constr env sigma = Constrintern.interp_constr sigma env
 
+(* Tactics *)
 let tclTHEN = Tacticals.tclTHEN
 let tclTHENLAST = Tacticals.tclTHENLAST
 let assert_before = Tactics.assert_tac
-
-let vm_conv = Reduction.vm_conv
 let vm_cast_no_check = Tactics.vm_cast_no_check
-let cbv_vm = Vnorm.cbv_vm
-
 let mk_tactic tac gl =
   let env = Tacmach.pf_env gl in
   let sigma = Tacmach.project gl in
@@ -123,6 +160,12 @@ let mk_tactic tac gl =
   tac env sigma t gl
 let set_evars_tac _ = Tacticals.tclIDTAC
 
+
+(* Other differences between the two versions of Coq *)
+let error = Errors.error
+let extern_constr = Constrextern.extern_constr true Environ.empty_env
+let destruct_rel_decl (n, _, t) = n, t
+let interp_constr env sigma = Constrintern.interp_constr sigma env
 let ppconstr_lsimpleconstr = Ppconstr.lsimple
 let constrextern_extern_constr =
   let env = Global.env () in
@@ -133,25 +176,7 @@ let get_rel_dec_name = fun _ -> Names.Anonymous
 (* Eta-expanded to get rid of optional arguments *)
 let retyping_get_type_of env = Retyping.get_type_of env
 
+let vm_conv = Reduction.vm_conv
+let cbv_vm = Vnorm.cbv_vm
 
-(* Micromega *)
-module Micromega_plugin_Certificate = Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega
-module Micromega_plugin_Micromega = Micromega
-module Micromega_plugin_Mutils = Mutils
-
-let micromega_coq_proofTerm =
-  Coq_micromega.M.coq_proofTerm
-
-let micromega_dump_proof_term p =
-  Coq_micromega.dump_proof_term p
-
-
-(* Types in the Coq source code *)
-type tactic = Proof_type.tactic
-type names_id = Names.identifier
-type constr_expr = Topconstr.constr_expr
 
-(* EConstr *)
-type econstr = Term.constr
-let econstr_of_constr e = e
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index 9ec21d2..abedc17 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -10,49 +10,74 @@
 (**************************************************************************)
 
 
-val gen_constant : string list list -> string -> Term.constr lazy_t
+(* Constr generation and manipulation *)
+type id
+val mkId : string -> id
+
+type name
+val name_of_id : id -> name
+val mkName : string -> name
+val string_of_name : name -> string
+
+type constr = Term.constr
+type types = constr
+val eq_constr : constr -> constr -> bool
+val hash_constr : constr -> int
+val mkProp : types
+val mkConst : Names.Constant.t -> constr
+val mkVar : id -> constr
+val mkRel : int -> constr
+val isRel : constr -> bool
+val destRel : constr -> int
+val lift : int -> constr -> constr
+val mkApp : constr -> constr array -> constr
+val decompose_app : constr -> constr * constr list
+val mkLambda : name * types * constr -> constr
+val mkProd : name * types * types -> types
+val mkLetIn : name * constr * types * constr -> constr
+
+val pr_constr_env : Environ.env -> constr -> Pp.t
+val pr_constr : constr -> Pp.t
+
+val mkUConst : constr -> Entries.definition_entry
+val mkTConst : constr -> 'a -> types -> Entries.definition_entry
+val declare_new_type : id -> types
+val declare_new_variable : id -> types -> constr
+val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t
+
+type cast_kind
+val vmcast : cast_kind
+val mkCast : constr * cast_kind * constr -> constr
+
+
+(* EConstr *)
+type econstr = constr
+val econstr_of_constr : constr -> econstr
+
+
+(* Modules *)
+val gen_constant : string list list -> string -> constr lazy_t
+
+
+(* Int63 *)
 val int63_modules : string list list
-val mkInt : int -> Term.constr
-val cint : Term.constr lazy_t
+val mkInt : int -> constr
+val cint : constr lazy_t
+
+
+(* PArray *)
 val parray_modules : string list list
 val max_array_size : int
-val mkArray : Term.types * Term.constr array -> Term.constr
+val mkArray : types * constr array -> constr
+
+
+(* Traces *)
 val mkTrace :
-  ('a -> Term.constr) ->
+  ('a -> constr) ->
   ('a -> 'a) ->
-  Term.constr Lazy.t ->
+  constr Lazy.t ->
   'b ->
-  'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr
-type names_id_t = Names.identifier
-val mkUConst : Term.constr -> Entries.definition_entry
-val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry
-val error : string -> 'a
-val coqtype : Term.types lazy_t
-val declare_new_type : Names.variable -> Term.constr
-val declare_new_variable : Names.variable -> Term.types -> Term.constr
-val extern_constr : Term.constr -> Topconstr.constr_expr
-val vernacentries_interp : Topconstr.constr_expr -> unit
-val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
-val lift : int -> Term.constr -> Term.constr
-val destruct_rel_decl : Term.rel_declaration -> Names.name * Term.constr
-val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> Term.constr
-val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
-val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
-val assert_before : Names.name -> Term.types -> Proof_type.tactic
-
-val vm_conv : Reduction.conv_pb -> Term.types Reduction.conversion_function
-val vm_cast_no_check : Term.constr -> Proof_type.tactic
-val cbv_vm : Environ.env -> Term.constr -> Term.types -> Term.constr
-
-val mk_tactic :
-  (Environ.env ->
-   Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) ->
-  Proof_type.goal Tacmach.sigma -> 'a
-val set_evars_tac : 'a -> Proof_type.tactic
-val ppconstr_lsimpleconstr : Ppconstr.precedence
-val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr
-val get_rel_dec_name : 'a -> Names.name
-val retyping_get_type_of : Environ.env -> Evd.evar_map -> Term.constr -> Term.constr
+  'c -> 'd -> 'e -> int -> types -> constr -> 'a ref -> constr
 
 
 (* Micromega *)
@@ -61,15 +86,33 @@ module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
 
-val micromega_coq_proofTerm : Term.constr lazy_t
-val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> Term.constr
+val micromega_coq_proofTerm : constr lazy_t
+val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
 
 
-(* Types in the Coq source code *)
+(* Tactics *)
 type tactic = Proof_type.tactic
-type names_id = Names.identifier
+val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+val assert_before : name -> types -> Proof_type.tactic
+val vm_cast_no_check : constr -> Proof_type.tactic
+val mk_tactic :
+  (Environ.env ->
+   Evd.evar_map -> types -> Proof_type.goal Tacmach.sigma -> 'a) ->
+  Proof_type.goal Tacmach.sigma -> 'a
+val set_evars_tac : 'a -> Proof_type.tactic
+
+
+(* Other differences between the two versions of Coq *)
 type constr_expr = Topconstr.constr_expr
+val error : string -> 'a
+val extern_constr : constr -> Topconstr.constr_expr
+val destruct_rel_decl : Term.rel_declaration -> name * constr
+val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr
+val ppconstr_lsimpleconstr : Ppconstr.precedence
+val constrextern_extern_constr : constr -> Topconstr.constr_expr
+val get_rel_dec_name : 'a -> name
+val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
 
-(* EConstr *)
-type econstr = Term.constr
-val econstr_of_constr : Term.constr -> econstr
+val vm_conv : Reduction.conv_pb -> types Reduction.conversion_function
+val cbv_vm : Environ.env -> constr -> types -> constr