aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/interface')
-rw-r--r--contrib/interface/ascent.mli2
-rw-r--r--contrib/interface/centaur.ml19
-rw-r--r--contrib/interface/ctast.ml15
-rw-r--r--contrib/interface/dad.ml3
-rw-r--r--contrib/interface/name_to_ast.ml43
-rw-r--r--contrib/interface/parse.ml22
-rw-r--r--contrib/interface/pbp.ml57
-rw-r--r--contrib/interface/showproof.ml121
-rw-r--r--contrib/interface/vtp.ml5
-rw-r--r--contrib/interface/xlate.ml21
10 files changed, 156 insertions, 152 deletions
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index 3dff01937..3b9d742e2 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -8,7 +8,7 @@ and ct_AST =
CT_coerce_ID_OR_INT_to_AST of ct_ID_OR_INT
| CT_coerce_ID_OR_STRING_to_AST of ct_ID_OR_STRING
| CT_astnode of ct_ID * ct_AST_LIST
- | CT_astpath of ct_ID_LIST * ct_ID
+ | CT_astpath of ct_ID_LIST
| CT_astslam of ct_ID_OPT * ct_AST
and ct_AST_LIST =
CT_ast_list of ct_AST list
diff --git a/contrib/interface/centaur.ml b/contrib/interface/centaur.ml
index 2f864b13e..bba7396b0 100644
--- a/contrib/interface/centaur.ml
+++ b/contrib/interface/centaur.ml
@@ -1,6 +1,7 @@
(*Toplevel loop for the communication between Coq and Centaur *)
open Names;;
+open Nameops
open Util;;
open Ast;;
open Term;;
@@ -243,8 +244,10 @@ let filter_by_module_from_varg_list (l:vernac_arg list) =
let add_search (global_reference:global_reference) assumptions cstr =
try
- let id_string = string_of_qualid (Global.qualid_of_global global_reference) in
- let ast =
+ let env = Global.env() in
+ let id_string =
+ string_of_qualid (Nametab.qualid_of_global env global_reference) in
+ let ast =
try
CT_premise (CT_ident id_string, translate_constr assumptions cstr)
with Not_found ->
@@ -303,11 +306,13 @@ and ntyp = nf_betaiota typ in
(* The following function is copied from globpr in env/printer.ml *)
let globcv = function
| Node(_,"MUTIND", (Path(_,sp))::(Num(_,tyi))::_) ->
- convert_qualid
- (Global.qualid_of_global (IndRef(sp,tyi)))
+ let env = Global.env() in
+ convert_qualid
+ (Nametab.qualid_of_global env (IndRef(sp,tyi)))
| Node(_,"MUTCONSTRUCT",(Path(_,sp))::(Num(_,tyi))::(Num(_,i))::_) ->
- convert_qualid
- (Global.qualid_of_global (ConstructRef ((sp, tyi), i)))
+ let env = Global.env() in
+ convert_qualid
+ (Nametab.qualid_of_global env (ConstructRef ((sp, tyi), i)))
| _ -> failwith "globcv : unexpected value";;
let pbp_tac_pcoq =
@@ -389,7 +394,7 @@ let inspect n =
sp, Lib.Leaf lobj ->
(match sp, object_tag lobj with
_, "VARIABLE" ->
- let ((_, _, v), _) = get_variable sp in
+ let ((_, _, v), _) = get_variable (basename sp) in
add_search2 (Nametab.locate (qualid_of_sp sp)) v
| sp, ("CONSTANT"|"PARAMETER") ->
let {const_type=typ} = Global.lookup_constant sp in
diff --git a/contrib/interface/ctast.ml b/contrib/interface/ctast.ml
index 5b97716fc..b356f5b28 100644
--- a/contrib/interface/ctast.ml
+++ b/contrib/interface/ctast.ml
@@ -11,15 +11,15 @@ type t =
| Num of loc * int
| Id of loc * string
| Str of loc * string
- | Path of loc * string list* string
+ | Path of loc * string list
| Dynamic of loc * Dyn.t
-let section_path sl k =
+let section_path sl =
match List.rev sl with
| s::pa ->
make_path
(make_dirpath (List.rev (List.map id_of_string pa)))
- (id_of_string s) (kind_of_string k)
+ (id_of_string s)
| [] -> invalid_arg "section_path"
let is_meta s = String.length s > 0 && s.[0] == '$'
@@ -40,7 +40,7 @@ let rec ct_to_ast = function
| Num (loc,a) -> Coqast.Num (loc,a)
| Id (loc,a) -> Coqast.Id (loc,a)
| Str (loc,a) -> Coqast.Str (loc,a)
- | Path (loc,sl,k) -> Coqast.Path (loc,section_path sl k)
+ | Path (loc,sl) -> Coqast.Path (loc,section_path sl)
| Dynamic (loc,a) -> Coqast.Dynamic (loc,a)
let rec ast_to_ct = function
@@ -55,8 +55,9 @@ let rec ast_to_ct = function
| Coqast.Id (loc,a) -> Id (loc,a)
| Coqast.Str (loc,a) -> Str (loc,a)
| Coqast.Path (loc,a) ->
- let (sl,bn,pk) = repr_path a in
- Path(loc, (List.map string_of_id (repr_dirpath sl)) @ [string_of_id bn],(* Bidon *) "CCI")
+ let (sl,bn) = repr_path a in
+ Path(loc, (List.map string_of_id
+ (List.rev (repr_dirpath sl))) @ [string_of_id bn])
| Coqast.Dynamic (loc,a) -> Dynamic (loc,a)
let loc = function
@@ -66,7 +67,7 @@ let loc = function
| Num (loc,_) -> loc
| Id (loc,_) -> loc
| Str (loc,_) -> loc
- | Path (loc,_,_) -> loc
+ | Path (loc,_) -> loc
| Dynamic (loc,_) -> loc
let str s = Str(Ast.dummy_loc,s)
diff --git a/contrib/interface/dad.ml b/contrib/interface/dad.ml
index f84fe33ef..7f2ea95a4 100644
--- a/contrib/interface/dad.ml
+++ b/contrib/interface/dad.ml
@@ -15,6 +15,7 @@ open Ctast;;
open Termast;;
open Astterm;;
open Vernacinterp;;
+open Nametab
open Proof_type;;
open Proof_trees;;
@@ -51,7 +52,7 @@ let zz = (0,0);;
let rec get_subterm (depth:int) (path: int list) (constr:constr) =
match depth, path, kind_of_term constr with
0, l, c -> (constr,l)
- | n, 2::a::tl, IsApp(func,arr) ->
+ | n, 2::a::tl, App(func,arr) ->
get_subterm (n - 2) tl arr.(a-1)
| _,l,_ -> failwith (int_list_to_string
"wrong path or wrong form of term"
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index e4523121c..8d3fd79c0 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -1,6 +1,7 @@
open Sign;;
open Classops;;
open Names;;
+open Nameops
open Coqast;;
open Ast;;
open Termast;;
@@ -15,6 +16,7 @@ open Inductive;;
open Util;;
open Pp;;
open Declare;;
+open Nametab
(* This function converts the parameter binders of an inductive definition,
@@ -86,8 +88,8 @@ let convert_qualid qid =
let d, id = Nametab.repr_qualid qid in
match repr_dirpath d with
[] -> nvar id
- | d -> ope("QUALID", List.fold_right (fun s l -> (nvar s)::l) d
- [nvar id]);;
+ | d -> ope("QUALID", List.fold_left (fun l s -> (nvar s)::l)
+ [nvar id] d);;
(* This function converts constructors for an inductive definition to a
Coqast.t. It is obtained directly from print_constructors in pretty.ml *)
@@ -106,9 +108,9 @@ let convert_constructors envpar names types =
let convert_one_inductive sp tyi =
let (ref, params, arity, cstrnames, cstrtypes) = build_inductive sp tyi in
let env = Global.env () in
- let envpar = push_rels params env in
+ let envpar = push_rel_context params env in
ope("VERNACARGLIST",
- [convert_qualid (Global.qualid_of_global(IndRef (sp, tyi)));
+ [convert_qualid (Nametab.qualid_of_global env (IndRef (sp, tyi)));
ope("CONSTR", [ast_of_constr true envpar arity]);
ope("BINDERLIST", convert_env(List.rev params));
convert_constructors envpar cstrnames cstrtypes]);;
@@ -123,7 +125,7 @@ let mutual_to_ast_list sp mib =
Array.fold_right
(fun mi (n,l) -> (n+1, (convert_one_inductive sp n)::l)) mipv (0, []) in
(ope("MUTUALINDUCTIVE",
- [str (if (mipv.(0)).mind_finite then "Inductive" else "CoInductive");
+ [str (if mib.mind_finite then "Inductive" else "CoInductive");
ope("VERNACARGLIST", ast_list)])::
(implicit_args_to_ast_list sp mipv));;
@@ -157,17 +159,14 @@ let make_definition_ast name c typ implicits =
(* This function is inspired by print_constant *)
let constant_to_ast_list sp =
let cb = Global.lookup_constant sp in
- if kind_of_path sp = CCI then
- let c = cb.const_body in
- let typ = cb.const_type in
- let l = constant_implicits_list sp in
- (match c with
- None ->
- make_variable_ast (basename sp) typ l
- | Some c1 ->
- make_definition_ast (basename sp) c1 typ l)
- else
- errorlabstrm "print" [< 'sTR "printing of FW terms not implemented" >];;
+ let c = cb.const_body in
+ let typ = cb.const_type in
+ let l = constant_implicits_list sp in
+ (match c with
+ None ->
+ make_variable_ast (basename sp) typ l
+ | Some c1 ->
+ make_definition_ast (basename sp) c1 typ l)
let variable_to_ast_list sp =
let ((id, c, v), _) = get_variable sp in
@@ -182,18 +181,14 @@ let variable_to_ast_list sp =
let inductive_to_ast_list sp =
let mib = Global.lookup_mind sp in
- if kind_of_path sp = CCI then
- mutual_to_ast_list sp mib
- else
- errorlabstrm "print"
- [< 'sTR "printing of FW not implemented" >];;
+ mutual_to_ast_list sp mib
(* this function is inspired by print_leaf_entry from pretty.ml *)
let leaf_entry_to_ast_list (sp,lobj) =
let tag = object_tag lobj in
match (sp,tag) with
- | (_, "VARIABLE") -> variable_to_ast_list sp
+ | (_, "VARIABLE") -> variable_to_ast_list (basename sp)
| (_, ("CONSTANT"|"PARAMETER")) -> constant_to_ast_list sp
| (_, "INDUCTIVE") -> inductive_to_ast_list sp
| (_, s) ->
@@ -228,8 +223,8 @@ let name_to_ast (qid:Nametab.qualid) =
with Not_found ->
try (* Var locale de but, pas var de section... donc pas d'implicits *)
let dir,name = Nametab.repr_qualid qid in
- if dir <> make_dirpath [] then raise Not_found;
- let (c,typ) = Global.lookup_named name in
+ if (repr_dirpath dir) <> [] then raise Not_found;
+ let (_,c,typ) = Global.lookup_named name in
(match c with
None -> make_variable_ast name typ []
| Some c1 -> make_definition_ast name c1 typ [])
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index 42daf3c19..6b2e38873 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -292,14 +292,9 @@ let parse_file_action reqid file_name =
(* This function is taken from Mltop.add_path *)
let add_path dir coq_dirpath =
-(*
- if coq_dirpath = Names.make_dirpath [] then
- anomaly "add_path: empty path in library";
-*)
if exists_dir dir then
begin
- Library.add_load_path_entry (dir,coq_dirpath);
- Nametab.push_library_root coq_dirpath
+ Library.add_load_path_entry (dir,coq_dirpath)
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >]
@@ -309,18 +304,15 @@ let convert_string d =
with _ -> failwith "caught"
let add_rec_path dir coq_dirpath =
-(*
- if coq_dirpath = Names.make_dirpath [] then anomaly "add_path: empty path in library";
-*)
let dirs = all_subdirs dir in
let prefix = Names.repr_dirpath coq_dirpath in
if dirs <> [] then
let convert_dirs (lp,cp) =
- (lp,Names.make_dirpath (prefix@(List.map convert_string cp))) in
+ (lp,
+ Names.make_dirpath ((List.map convert_string (List.rev cp))@prefix)) in
let dirs = map_succeed convert_dirs dirs in
begin
- List.iter Library.add_load_path_entry dirs;
- Nametab.push_library_root coq_dirpath
+ List.iter Library.add_load_path_entry dirs
end
else
wARNING [< 'sTR ("Cannot open " ^ dir) >];;
@@ -380,9 +372,9 @@ Libobject.relax true;
else
(mSGNL [< 'sTR "could not find the value of COQDIR" >]; exit 1) in
begin
- add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nametab.coq_root]);
- add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nametab.coq_root]);
- add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nametab.coq_root]);
+ add_rec_path (Filename.concat coqdir "theories") (Names.make_dirpath [Nameops.coq_root]);
+ add_path (Filename.concat coqdir "tactics") (Names.make_dirpath [Nameops.coq_root]);
+ add_rec_path (Filename.concat coqdir "contrib") (Names.make_dirpath [Nameops.coq_root]);
List.iter (fun a -> mSGNL [< 'sTR a >]) (get_load_path())
end;
(try
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 4ece713f5..13e307a47 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -75,7 +75,7 @@ let make_final_cmd f optname clear_names constr path =
add_clear_names_if_necessary (f optname constr path) clear_names;;
let (rem_cast:pbp_rule) = function
- (a,c,cf,o, IsCast(f,_), p, func) ->
+ (a,c,cf,o, Cast(f,_), p, func) ->
Some(func a c cf o (kind_of_term f) p)
| _ -> None;;
@@ -84,7 +84,7 @@ let (forall_intro: pbp_rule) = function
clear_names,
clear_flag,
None,
- IsProd(Name x, _, body),
+ Prod(Name x, _, body),
(2::path),
f) ->
let x' = next_global_ident_away x avoid in
@@ -95,7 +95,7 @@ let (forall_intro: pbp_rule) = function
let (imply_intro2: pbp_rule) = function
avoid, clear_names,
- clear_flag, None, IsProd(Anonymous, _, body), 2::path, f ->
+ clear_flag, None, Prod(Anonymous, _, body), 2::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
Some(Node(zz, "TACTICLIST",
[make_named_intro (string_of_id h');
@@ -105,7 +105,7 @@ let (imply_intro2: pbp_rule) = function
let (imply_intro1: pbp_rule) = function
avoid, clear_names,
- clear_flag, None, IsProd(Anonymous, prem, body), 1::path, f ->
+ clear_flag, None, Prod(Anonymous, prem, body), 1::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
let str_h' = (string_of_id h') in
Some(Node(zz, "TACTICLIST",
@@ -117,7 +117,7 @@ let (imply_intro1: pbp_rule) = function
let (forall_elim: pbp_rule) = function
avoid, clear_names, clear_flag,
- Some h, IsProd(Name x, _, body), 2::path, f ->
+ Some h, Prod(Name x, _, body), 2::path, f ->
let h' = next_global_ident_away (id_of_string "H") avoid in
let clear_names' = if clear_flag then h::clear_names else clear_names in
let str_h' = (string_of_id h') in
@@ -135,7 +135,7 @@ let (forall_elim: pbp_rule) = function
let (imply_elim1: pbp_rule) = function
avoid, clear_names, clear_flag,
- Some h, IsProd(Anonymous, prem, body), 1::path, f ->
+ Some h, Prod(Anonymous, prem, body), 1::path, f ->
let clear_names' = if clear_flag then h::clear_names else clear_names in
let h' = next_global_ident_away (id_of_string "H") avoid in
let str_h' = (string_of_id h') in
@@ -156,7 +156,7 @@ let (imply_elim1: pbp_rule) = function
let (imply_elim2: pbp_rule) = function
avoid, clear_names, clear_flag,
- Some h, IsProd(Anonymous, prem, body), 2::path, f ->
+ Some h, Prod(Anonymous, prem, body), 2::path, f ->
let clear_names' = if clear_flag then h::clear_names else clear_names in
let h' = next_global_ident_away (id_of_string "H") avoid in
let str_h' = (string_of_id h') in
@@ -176,7 +176,8 @@ let (imply_elim2: pbp_rule) = function
| _ -> None;;
let reference dir s =
- let dir = make_dirpath (List.map id_of_string ("Coq"::"Init"::[dir])) in
+ let dir = make_dirpath
+ (List.map id_of_string (List.rev ("Coq"::"Init"::[dir]))) in
let id = id_of_string s in
try
Nametab.locate_in_absolute_module dir id
@@ -204,7 +205,7 @@ let is_matching_local a b = is_matching (pattern_of_constr a) b;;
let (and_intro: pbp_rule) = function
avoid, clear_names, clear_flag,
- None, IsApp(and_oper, [|c1; c2|]), 2::a::path, f
+ None, App(and_oper, [|c1; c2|]), 2::a::path, f
->
if ((is_matching_local (andconstr()) and_oper) or
(is_matching_local (prodconstr ()) and_oper)) & (a = 1 or a = 2) then
@@ -229,12 +230,12 @@ let (and_intro: pbp_rule) = function
let (ex_intro: pbp_rule) = function
avoid, clear_names, clear_flag, None,
- IsApp(oper, [| c1; c2|]), 2::2::2::path, f
+ App(oper, [| c1; c2|]), 2::2::2::path, f
when (is_matching_local (exconstr ()) oper) or (is_matching_local (exTconstr ()) oper)
or (is_matching_local (sigconstr ()) oper)
or (is_matching_local (sigTconstr ()) oper) ->
(match kind_of_term c2 with
- IsLambda(Name x, _, body) ->
+ Lambda(Name x, _, body) ->
Some(Node(zz, "Split",
[Node(zz, "BINDINGS",
[Node(zz, "BINDING",
@@ -250,7 +251,7 @@ let (ex_intro: pbp_rule) = function
let (or_intro: pbp_rule) = function
avoid, clear_names, clear_flag, None,
- IsApp(or_oper, [|c1; c2 |]), 2::a::path, f ->
+ App(or_oper, [|c1; c2 |]), 2::a::path, f ->
if ((is_matching_local (orconstr ()) or_oper) or
(is_matching_local (sumboolconstr ()) or_oper) or
(is_matching_local (sumconstr ()) or_oper))
@@ -270,7 +271,7 @@ let dummy_id = id_of_string "Dummy";;
let (not_intro: pbp_rule) = function
avoid, clear_names, clear_flag, None,
- IsApp(not_oper, [|c1|]), 2::1::path, f ->
+ App(not_oper, [|c1|]), 2::1::path, f ->
if(is_matching_local (notconstr ()) not_oper) or
(is_matching_local (notTconstr ()) not_oper) then
let h' = next_global_ident_away (id_of_string "H") avoid in
@@ -336,11 +337,11 @@ let rec down_prods: (types, constr) kind_of_term * (int list) * int ->
string list * (int list) * int * (types, constr) kind_of_term *
(int list) =
function
- IsProd(Name x, _, body), 2::path, k ->
+ Prod(Name x, _, body), 2::path, k ->
let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
(string_of_id x)::res_sl, (k::res_il), res_i, res_cstr, res_p
- | IsProd(Anonymous, _, body), 2::path, k ->
+ | Prod(Anonymous, _, body), 2::path, k ->
let res_sl, res_il, res_i, res_cstr, res_p
= down_prods (kind_of_term body, path, k+1) in
res_sl, res_il, res_i+1, res_cstr, res_p
@@ -361,14 +362,14 @@ let (check_apply: (types, constr) kind_of_term -> (int list) -> bool) =
| [] -> []
| p::tl -> if n = p then tl else p::(delete n tl) in
let rec check_rec l = function
- | IsApp(f, array) ->
+ | App(f, array) ->
Array.fold_left (fun l c -> check_rec l (kind_of_term c))
(check_rec l (kind_of_term f)) array
- | IsConst _ -> l
- | IsMutInd _ -> l
- | IsMutConstruct _ -> l
- | IsVar _ -> l
- | IsRel p ->
+ | Const _ -> l
+ | Ind _ -> l
+ | Construct _ -> l
+ | Var _ -> l
+ | Rel p ->
let result = delete p l in
if result = [] then
raise (Pbp_internal [])
@@ -399,7 +400,7 @@ let (head_tactic_patt: pbp_rule) = function
avoid, clear_names, clear_flag, Some h, cstr, path, f ->
(match down_prods (cstr, path, 0) with
| (str_list, _, nprems,
- IsApp(oper,[|c1|]), 2::1::path)
+ App(oper,[|c1|]), 2::1::path)
when
(is_matching_local (notconstr ()) oper) or
(is_matching_local (notTconstr ()) oper) ->
@@ -407,7 +408,7 @@ let (head_tactic_patt: pbp_rule) = function
[elim_with_bindings h str_list;
f avoid clear_names false None (kind_of_term c1) path]))
| (str_list, _, nprems,
- IsApp(oper, [|c1; c2|]), 2::a::path)
+ App(oper, [|c1; c2|]), 2::a::path)
when ((is_matching_local (andconstr()) oper) or
(is_matching_local (prodconstr()) oper)) & (a = 1 or a = 2) ->
let h1 = next_global_ident_away (id_of_string "H") avoid in
@@ -431,18 +432,18 @@ let (head_tactic_patt: pbp_rule) = function
cont_tac::(auxiliary_goals
clear_names clear_flag
h nprems))]))
- | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path)
+ | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
when ((is_matching_local (exconstr ()) oper) or
(is_matching_local (exTconstr ()) oper) or
(is_matching_local (sigconstr ()) oper) or
(is_matching_local (sigTconstr()) oper)) & a = 2 ->
(match (kind_of_term c2),path with
- IsLambda(Name x, _,body), (2::path) ->
+ Lambda(Name x, _,body), (2::path) ->
Some(Node(zz,"TACTICLIST",
[elim_with_bindings h str_list;
let x' = next_global_ident_away x avoid in
let cont_body =
- IsProd(Name x', c1,
+ Prod(Name x', c1,
mkProd(Anonymous, body,
mkVar(dummy_id))) in
let cont_tac
@@ -456,7 +457,7 @@ let (head_tactic_patt: pbp_rule) = function
clear_names clear_flag
h nprems))]))
| _ -> None)
- | (str_list, _, nprems, IsApp(oper,[|c1; c2|]), 2::a::path)
+ | (str_list, _, nprems, App(oper,[|c1; c2|]), 2::a::path)
when ((is_matching_local (orconstr ()) oper) or
(is_matching_local (sumboolconstr ()) oper) or
(is_matching_local (sumconstr ()) oper)) &
@@ -491,7 +492,7 @@ let (head_tactic_patt: pbp_rule) = function
false "dummy" nprems))]))
| (str_list, int_list, nprems, c, [])
when (check_apply c (mk_db_indices int_list nprems)) &
- (match c with IsProd(_,_,_) -> false
+ (match c with Prod(_,_,_) -> false
| _ -> true) &
(List.length int_list) + nprems > 0 ->
Some(add_clear_names_if_necessary
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 50aebb917..e4d4647f1 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -5,19 +5,22 @@ open Coqast;;
open Environ
open Evd
open Names
+open Nameops
open Stamps
open Term
+open Termops
open Util
open Proof_type
open Coqast
open Pfedit
open Translate
open Term
-open Reduction
+open Reductionops
open Clenv
open Astterm
open Typing
open Inductive
+open Inductiveops
open Vernacinterp
open Declarations
open Showproof_ct
@@ -205,7 +208,7 @@ let fill_unproved nt l =
let new_sign osign sign =
let res=ref [] in
List.iter (fun (id,c,ty) ->
- try (let ty1= (lookup_id_type id osign) in
+ try (let (_,_,ty1)= (lookup_named id osign) in
())
with Not_found -> res:=(id,c,ty)::(!res))
sign;
@@ -215,7 +218,7 @@ let new_sign osign sign =
let old_sign osign sign =
let res=ref [] in
List.iter (fun (id,c,ty) ->
- try (let ty1= (lookup_id_type id osign) in
+ try (let (_,_,ty1) = (lookup_named id osign) in
if ty1 = ty then res:=(id,c,ty)::(!res))
with Not_found -> ())
sign;
@@ -711,7 +714,7 @@ let sort_of_type t ts =
match ts with
Prop(Null) -> Nformula
|_ -> (match (kind_of_term t) with
- IsProd(_,_,_) -> Nfunction
+ Prod(_,_,_) -> Nfunction
|_ -> Ntype)
;;
@@ -722,22 +725,22 @@ let adrel (x,t) e =
let rec nsortrec vl x =
match (kind_of_term x) with
- IsProd(n,t,c)->
+ Prod(n,t,c)->
let vl = (adrel (n,t) vl) in nsortrec vl c
- | IsLambda(n,t,c) ->
+ | Lambda(n,t,c) ->
let vl = (adrel (n,t) vl) in nsortrec vl c
- | IsApp(f,args) -> nsortrec vl f
- | IsSort(Prop(Null)) -> Prop(Null)
- | IsSort(c) -> c
- | IsMutInd(ind) ->
- let dmi = lookup_mind_specif ind vl in
- (mis_sort dmi)
- | IsMutConstruct(c) ->
- nsortrec vl (mkMutInd (inductive_of_constructor c))
- | IsMutCase(_,x,t,a)
+ | App(f,args) -> nsortrec vl f
+ | Sort(Prop(Null)) -> Prop(Null)
+ | Sort(c) -> c
+ | Ind(ind) ->
+ let (mib,mip) = lookup_mind_specif vl ind in
+ mip.mind_sort
+ | Construct(c) ->
+ nsortrec vl (mkInd (inductive_of_constructor c))
+ | Case(_,x,t,a)
-> nsortrec vl x
- | IsCast(x,t)-> nsortrec vl t
- | IsConst c -> nsortrec vl (lookup_constant c vl).const_type
+ | Cast(x,t)-> nsortrec vl t
+ | Const c -> nsortrec vl (lookup_constant c vl).const_type
| _ -> nsortrec vl (type_of vl Evd.empty x)
;;
let nsort x =
@@ -1056,7 +1059,7 @@ let first_name_hyp_of_ntree {t_goal={newhyp=lh}}=
let rec find_type x t=
match (kind_of_term (strip_outer_cast t)) with
- IsProd(y,ty,t) ->
+ Prod(y,ty,t) ->
(match y with
Name y ->
if x=(string_of_id y) then ty
@@ -1071,9 +1074,9 @@ Traitement des égalités
(*
let is_equality e =
match (kind_of_term e) with
- IsAppL args ->
+ AppL args ->
(match (kind_of_term args.(0)) with
- IsConst (c,_) ->
+ Const (c,_) ->
(match (string_of_sp c) with
"Equal" -> true
| "eq" -> true
@@ -1088,14 +1091,14 @@ let is_equality e =
let is_equality e =
let e= (strip_outer_cast e) in
match (kind_of_term e) with
- IsApp (f,args) -> (Array.length args) >= 3
+ App (f,args) -> (Array.length args) >= 3
| _ -> false
;;
let terms_of_equality e =
let e= (strip_outer_cast e) in
match (kind_of_term e) with
- IsApp (f,args) -> (args.(1) , args.(2))
+ App (f,args) -> (args.(1) , args.(2))
| _ -> assert false
;;
@@ -1404,22 +1407,24 @@ and whd_betadeltaiota x = whd_betaiotaevar (Global.env()) Evd.empty x
and type_of_ast s c = type_of (Global.env()) Evd.empty (constr_of_ast c)
and prod_head t =
match (kind_of_term (strip_outer_cast t)) with
- IsProd(_,_,c) -> prod_head c
-(* |IsApp(f,a) -> f *)
+ Prod(_,_,c) -> prod_head c
+(* |App(f,a) -> f *)
| _ -> t
and string_of_sp sp = string_of_id (basename sp)
-and constr_of_mind dmi i = (string_of_id (mis_consnames dmi).(i-1))
-and arity_of_constr_of_mind indf i =
- (get_constructors indf).(i-1).cs_nargs
+and constr_of_mind mip i =
+ (string_of_id mip.mind_consnames.(i-1))
+and arity_of_constr_of_mind env indf i =
+ (get_constructors env indf).(i-1).cs_nargs
and gLOB ge = Global.env_of_context ge (* (Global.env()) *)
and natural_case ig lh g gs ge arg1 ltree with_intros =
let env= (gLOB ge) in
let targ1 = prod_head (type_of env Evd.empty arg1) in
let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
let type_arg= targ1 (* List.nth targ (mis_index dmi)*) in
if ncti<>1
(* Zéro ou Plusieurs constructeurs *)
@@ -1436,9 +1441,9 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
(let ci=ref 0 in
(prli
(fun treearg -> ci:=!ci+1;
- let nci=(constr_of_mind dmi !ci) in
+ let nci=(constr_of_mind mip !ci) in
let aci=if with_intros
- then (arity_of_constr_of_mind indf !ci)
+ then (arity_of_constr_of_mind env indf !ci)
else 0 in
let ici= (!ci) in
sph[ (natural_ntree
@@ -1464,10 +1469,10 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
(show_goal2 lh ig g gs "");
de_A_on_a arg1;
(let treearg=List.hd ltree in
- let nci=(constr_of_mind dmi 1) in
+ let nci=(constr_of_mind mip 1) in
let aci=
if with_intros
- then (arity_of_constr_of_mind indf 1)
+ then (arity_of_constr_of_mind env indf 1)
else 0 in
let ici= 1 in
sph[ (natural_ntree
@@ -1493,21 +1498,25 @@ and natural_case ig lh g gs ge arg1 ltree with_intros =
*)
and prod_list_var t =
match (kind_of_term (strip_outer_cast t)) with
- IsProd(_,t,c) -> t::(prod_list_var c)
+ Prod(_,t,c) -> t::(prod_list_var c)
|_ -> []
and hd_is_mind t ti =
- try (let IndType (indf,targ) = find_rectype (Global.env()) Evd.empty t in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- (string_of_id (mis_typename dmi)) = ti)
+ try (let env = Global.env() in
+ let IndType (indf,targ) = find_rectype env Evd.empty t in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ (string_of_id mip.mind_typename) = ti)
with _ -> false
and mind_ind_info_hyp_constr indf c =
- let IndFamily(dmi,_) = indf in
- let p= mis_nparams dmi in
- let a=arity_of_constr_of_mind indf c in
- let lp=ref (get_constructors indf).(c).cs_args in
+ let env = Global.env() in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let p = mip.mind_nparams in
+ let a = arity_of_constr_of_mind env indf c in
+ let lp=ref (get_constructors env indf).(c).cs_args in
let lr=ref [] in
- let ti = (string_of_id (mis_typename dmi)) in
+ let ti = (string_of_id mip.mind_typename) in
for i=1 to a do
match !lp with
((_,_,t)::lp1)->
@@ -1530,9 +1539,10 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
let env= (gLOB ge) in
let targ1 = prod_head (type_of env Evd.empty arg1) in
let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
let type_arg=targ1 (* List.nth targ (mis_index dmi) *) in
spv
[ (natural_lhyp lh ig.ihsg);
@@ -1543,8 +1553,8 @@ and natural_elim ig lh g gs ge arg1 ltree with_intros=
(let ci=ref 0 in
(prli
(fun treearg -> ci:=!ci+1;
- let nci=(constr_of_mind dmi !ci) in
- let aci=(arity_of_constr_of_mind indf !ci) in
+ let nci=(constr_of_mind mip !ci) in
+ let aci=(arity_of_constr_of_mind env indf !ci) in
let hci=
if with_intros
then mind_ind_info_hyp_constr indf !ci
@@ -1575,13 +1585,14 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
let env = (gLOB (g_env (List.hd ltree))) in
let arg1=dbize env arg1 in
let arg2 = match (kind_of_term arg1) with
- IsVar(arg2) -> arg2
+ Var(arg2) -> arg2
| _ -> assert false in
let targ1 = prod_head (type_of env Evd.empty arg1) in
let IndType (indf,targ) = find_rectype env Evd.empty targ1 in
- let ncti= Array.length(get_constructors indf) in
- let IndFamily(dmi,_) = indf in
- let ti =(string_of_id (mis_typename dmi)) in
+ let ncti= Array.length(get_constructors env indf) in
+ let (ind,_) = indf in
+ let (mib,mip) = lookup_mind_specif env ind in
+ let ti =(string_of_id mip.mind_typename) in
let type_arg= targ1(*List.nth targ (mis_index dmi)*) in
let lh1= hyps (List.hd ltree) in (* la liste des hyp jusqu'a n *)
@@ -1604,8 +1615,8 @@ and natural_induction ig lh g gs ge arg1 ltree with_intros=
(let ci=ref 0 in
(prli
(fun treearg -> ci:=!ci+1;
- let nci=(constr_of_mind dmi !ci) in
- let aci=(arity_of_constr_of_mind indf !ci) in
+ let nci=(constr_of_mind mip !ci) in
+ let aci=(arity_of_constr_of_mind env indf !ci) in
let hci=
if with_intros
then mind_ind_info_hyp_constr indf !ci
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index e35b9d3bc..778220322 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -26,10 +26,9 @@ and fAST = function
fID x1;
fAST_LIST x2;
fNODE "astnode" 2
-| CT_astpath(x1, x2) ->
+| CT_astpath(x1) ->
fID_LIST x1;
- fID x2;
- fNODE "astpath" 2
+ fNODE "astpath" 1
| CT_astslam(x1, x2) ->
fID_OPT x1;
fAST x2;
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index ccaa08f50..c7552847f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -381,18 +381,18 @@ let xlate_op the_node opn a b =
*)
"CONST" ->
(match a, b with
- | ((Path (_, sl, kind)) :: []), [] ->
+ | ((Path (_, sl)) :: []), [] ->
CT_coerce_ID_to_FORMULA(CT_ident
- (Names.string_of_id (Names.basename (section_path sl kind))))
- | ((Path (_, sl, kind)) :: []), tl ->
+ (Names.string_of_id (Nameops.basename (section_path sl))))
+ | ((Path (_, sl)) :: []), tl ->
CT_coerce_ID_to_FORMULA(CT_ident
- (Names.string_of_id(Names.basename (section_path sl kind))))
+ (Names.string_of_id(Nameops.basename (section_path sl))))
| _, _ -> xlate_error "xlate_op : CONST")
| (** string_of_path needs to be investigated.
*)
"MUTIND" ->
(match a, b with
- | [Path(_, sl, kind); Num(_, tyi)], [] ->
+ | [Path(_, sl); Num(_, tyi)], [] ->
if !in_coq_ref then
match special_case_qualid ()
(!xlate_mut_stuff (Node((0,0),"MUTIND", a))) with
@@ -401,8 +401,7 @@ let xlate_op the_node opn a b =
else
CT_coerce_ID_to_FORMULA(
CT_ident(Names.string_of_id
- (Names.basename
- (section_path sl kind))))
+ (Nameops.basename (section_path sl))))
| _, _ -> xlate_error "xlate_op : MUTIND")
| "MUTCASE"
| "CASE" ->
@@ -417,7 +416,7 @@ let xlate_op the_node opn a b =
*)
"MUTCONSTRUCT" ->
(match a, b with
- | [Path(_, sl, kind);Num(_, tyi);Num(_, n)], cl ->
+ | [Path(_, sl);Num(_, tyi);Num(_, n)], cl ->
if !in_coq_ref then
match
special_case_qualid ()
@@ -425,7 +424,7 @@ let xlate_op the_node opn a b =
| Some(Rform x) -> x
| _ -> assert false
else
- let name = Names.string_of_path (section_path sl kind) in
+ let name = Names.string_of_path (section_path sl) in
(* This is rather a patch to cope with the fact that identifier
names have disappeared from the vo files for grammar rules *)
let type_desc = (try Some (Hashtbl.find type_table name) with
@@ -1512,9 +1511,9 @@ let xlate_ast =
CT_coerce_ID_OR_STRING_to_AST
(CT_coerce_STRING_to_ID_OR_STRING (CT_string s))
| Dynamic(_,_) -> failwith "Dynamics not treated in xlate_ast"
- | Path (_, sl, s) ->
+ | Path (_, sl) ->
CT_astpath
- (CT_id_list (List.map (function s -> CT_ident s) sl), CT_ident s) in
+ (CT_id_list (List.map (function s -> CT_ident s) sl)) in
xlate_ast_aux;;
let get_require_flags impexp spec =
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-31 02:00:32 +0000