aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/printer.ml10
-rw-r--r--plugins/interface/depends.ml8
-rw-r--r--plugins/xml/proofTree2Xml.ml44
-rw-r--r--proofs/logic.ml27
-rw-r--r--proofs/proof_type.ml4
-rw-r--r--proofs/proof_type.mli4
-rw-r--r--proofs/tacmach.ml8
-rw-r--r--proofs/tacmach.mli4
-rw-r--r--tactics/hiddentac.ml4
-rw-r--r--tactics/refine.ml11
-rw-r--r--tactics/tactics.ml8
-rw-r--r--tactics/tactics.mli4
12 files changed, 52 insertions, 44 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml
index 267d550a9..37083eb46 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -427,10 +427,11 @@ let pr_prim_rule = function
(str"cut " ++ pr_constr t ++
str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]")
- | FixRule (f,n,[]) ->
+ | FixRule (f,n,[],_) ->
(str"fix " ++ pr_id f ++ str"/" ++ int n)
- | FixRule (f,n,others) ->
+ | FixRule (f,n,others,j) ->
+ if j<>0 then warning "Unsupported printing of \"fix\"";
let rec print_mut = function
| (f,n,ar)::oth ->
pr_id f ++ str"/" ++ int n ++ str" : " ++ pr_lconstr ar ++ print_mut oth
@@ -438,10 +439,11 @@ let pr_prim_rule = function
(str"fix " ++ pr_id f ++ str"/" ++ int n ++
str" with " ++ print_mut others)
- | Cofix (f,[]) ->
+ | Cofix (f,[],_) ->
(str"cofix " ++ pr_id f)
- | Cofix (f,others) ->
+ | Cofix (f,others,j) ->
+ if j<>0 then warning "Unsupported printing of \"fix\"";
let rec print_mut = function
| (f,ar)::oth ->
(pr_id f ++ str" : " ++ pr_lconstr ar ++ print_mut oth)
diff --git a/plugins/interface/depends.ml b/plugins/interface/depends.ml
index 378f9972e..445b193f8 100644
--- a/plugins/interface/depends.ml
+++ b/plugins/interface/depends.ml
@@ -58,8 +58,8 @@ let explore_tree pfs =
| Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
| Intro identifier -> "Intro"
| Cut (bool, _, identifier, types) -> "Cut"
- | FixRule (identifier, int, l) -> "FixRule"
- | Cofix (identifier, l) -> "Cofix"
+ | FixRule (identifier, int, l, _) -> "FixRule"
+ | Cofix (identifier, l, _) -> "Cofix"
| Convert_concl (types, cast_kind) -> "Convert_concl"
| Convert_hyp named_declaration -> "Convert_hyp"
| Thin identifier_list -> "Thin"
@@ -411,8 +411,8 @@ and depends_of_prim_rule pr acc = match pr with
| Refine c -> depends_of_constr c acc
| Intro id -> acc
| Cut (_, _, _, t) -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
- | FixRule (_, _, l) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
- | Cofix (_, l) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
+ | FixRule (_, _, l, _) -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
+ | Cofix (_, l, _) -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
| Convert_concl (t, _) -> depends_of_constr t acc
| Convert_hyp (_, None, t) -> depends_of_constr t acc
| Convert_hyp (_, (Some c), t) -> depends_of_constr c (depends_of_constr t acc)
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index a501fb6a6..7503d6328 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.ml4
@@ -82,8 +82,8 @@ let first_word s =
let string_of_prim_rule x = match x with
| Proof_type.Intro _-> "Intro"
| Proof_type.Cut _ -> "Cut"
- | Proof_type.FixRule (_,_,_) -> "FixRule"
- | Proof_type.Cofix (_,_)-> "Cofix"
+ | Proof_type.FixRule _ -> "FixRule"
+ | Proof_type.Cofix _ -> "Cofix"
| Proof_type.Refine _ -> "Refine"
| Proof_type.Convert_concl _ -> "Convert_concl"
| Proof_type.Convert_hyp _->"Convert_hyp"
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2cca258b9..b8ba88185 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -517,7 +517,7 @@ let prim_refiner r sigma goal =
let sg2 = mk_goal sign cl in
if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
- | FixRule (f,n,rest) ->
+ | FixRule (f,n,rest,j) ->
let rec check_ind env k cl =
match kind_of_term (strip_outer_cast cl) with
| Prod (na,c1,b) ->
@@ -531,7 +531,8 @@ let prim_refiner r sigma goal =
| _ -> error "Not enough products."
in
let (sp,_) = check_ind env n cl in
- let all = (f,n,cl)::rest in
+ let firsts,lasts = list_chop j rest in
+ let all = firsts@(f,n,cl)::lasts in
let rec mk_sign sign = function
| (f,n,ar)::oth ->
let (sp',_) = check_ind env n ar in
@@ -539,14 +540,15 @@ let prim_refiner r sigma goal =
error ("Fixpoints should be on the same " ^
"mutual inductive declaration.");
if !check && mem_named_context f (named_context_of_val sign) then
- error "Name already used in the environment";
+ error
+ ("Name "^string_of_id f^" already used in the environment");
mk_sign (push_named_context_val (f,None,ar) sign) oth
| [] ->
List.map (fun (_,_,c) -> mk_goal sign c) all
in
(mk_sign sign all, sigma)
- | Cofix (f,others) ->
+ | Cofix (f,others,j) ->
let rec check_is_coind env cl =
let b = whd_betadeltaiota env sigma cl in
match kind_of_term b with
@@ -558,7 +560,8 @@ let prim_refiner r sigma goal =
error ("All methods must construct elements " ^
"in coinductive types.")
in
- let all = (f,cl)::others in
+ let firsts,lasts = list_chop j others in
+ let all = firsts@(f,cl)::lasts in
List.iter (fun (_,c) -> check_is_coind env c) all;
let rec mk_sign sign = function
| (f,ar)::oth ->
@@ -687,24 +690,26 @@ let prim_extractor subfun vl pft =
mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
subfun (add_proof_var id vl) spf2)
- | Some (Prim (FixRule (f,n,others)),spfl) ->
- let all = Array.of_list ((f,n,cl)::others) in
+ | Some (Prim (FixRule (f,n,others,j)),spfl) ->
+ let firsts,lasts = list_chop j others in
+ let all = Array.of_list (firsts@(f,n,cl)::lasts) in
let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in
let names = Array.map (fun (f,_,_) -> Name f) all in
let vn = Array.map (fun (_,n,_) -> n-1) all in
let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl)
(add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkFix ((vn,0),(names,lcty,lfix))
+ mkFix ((vn,j),(names,lcty,lfix))
- | Some (Prim (Cofix (f,others)),spfl) ->
- let all = Array.of_list ((f,cl)::others) in
+ | Some (Prim (Cofix (f,others,j)),spfl) ->
+ let firsts,lasts = list_chop j others in
+ let all = Array.of_list (firsts@(f,cl)::lasts) in
let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in
let names = Array.map (fun (f,_) -> Name f) all in
let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl)
(add_proof_var f vl) others in
let lfix = Array.map (subfun newvl) (Array.of_list spfl) in
- mkCoFix (0,(names,lcty,lfix))
+ mkCoFix (j,(names,lcty,lfix))
| Some (Prim (Refine c),spfl) ->
let mvl = collect_meta_variables c in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 9f81ffee7..8a466d8df 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -29,8 +29,8 @@ open Pattern
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list
- | Cofix of identifier * (identifier * constr) list
+ | FixRule of identifier * int * (identifier * int * constr) list * int
+ | Cofix of identifier * (identifier * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5fb463da7..9db87d22e 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -29,8 +29,8 @@ open Pattern
type prim_rule =
| Intro of identifier
| Cut of bool * bool * identifier * types
- | FixRule of identifier * int * (identifier * int * constr) list
- | Cofix of identifier * (identifier * constr) list
+ | FixRule of identifier * int * (identifier * int * constr) list * int
+ | Cofix of identifier * (identifier * constr) list * int
| Refine of constr
| Convert_concl of types * cast_kind
| Convert_hyp of named_declaration
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index fa22de7bb..40917b085 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -214,11 +214,11 @@ let rec rename_hyp_no_check l gl = match l with
tclTHEN (refiner (Prim (Rename (id1,id2))))
(rename_hyp_no_check l) gl
-let mutual_fix f n others gl =
- with_check (refiner (Prim (FixRule (f,n,others)))) gl
+let mutual_fix f n others j gl =
+ with_check (refiner (Prim (FixRule (f,n,others,j)))) gl
-let mutual_cofix f others gl =
- with_check (refiner (Prim (Cofix (f,others)))) gl
+let mutual_cofix f others j gl =
+ with_check (refiner (Prim (Cofix (f,others,j)))) gl
(* Versions with consistency checks *)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 826337cc8..581933c83 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -139,8 +139,8 @@ val move_hyp_no_check :
val rename_hyp_no_check : (identifier*identifier) list -> tactic
val order_hyps : identifier list -> tactic
val mutual_fix :
- identifier -> int -> (identifier * int * constr) list -> tactic
-val mutual_cofix : identifier -> (identifier * constr) list -> tactic
+ identifier -> int -> (identifier * int * constr) list -> int -> tactic
+val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic
(*s The most primitive tactics with consistency and type checking *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 2aff94b64..4b89cbcb4 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -55,13 +55,13 @@ let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
let h_mutual_fix b id n l =
abstract_tactic
(TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
- (mutual_fix id n l)
+ (mutual_fix id n l 0)
let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
let h_mutual_cofix b id l =
abstract_tactic
(TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l))
- (mutual_cofix id l)
+ (mutual_cofix id l 0)
let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c)
let h_generalize_gen cl =
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 46c8d3aa2..f1ecc4da9 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -330,29 +330,30 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
gl
(* fix => tactique Fix *)
- | Fix ((ni,_),(fi,ai,_)) , _ ->
+ | Fix ((ni,j),(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
+ let firsts,lasts = list_chop j (Array.to_list fixes) in
tclTHENS
- (mutual_fix (out_name fi.(0)) (succ ni.(0))
- (List.tl (Array.to_list fixes)))
+ (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j)
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
gl
(* cofix => tactique CoFix *)
- | CoFix (_,(fi,ai,_)) , _ ->
+ | CoFix (j,(fi,ai,_)) , _ ->
let out_name = function
| Name id -> id
| _ -> error "Recursive functions must have names."
in
let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
+ let firsts,lasts = list_chop j (Array.to_list cofixes) in
tclTHENS
- (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
+ (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
(List.map (function
| None -> tclIDTAC
| Some th -> tcc_aux subst th) sgp)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3d3b22045..c3c1c4505 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -174,18 +174,18 @@ let mutual_fix = Tacmach.mutual_fix
let fix ido n gl = match ido with
| None ->
- mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] gl
+ mutual_fix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) n [] 0 gl
| Some id ->
- mutual_fix id n [] gl
+ mutual_fix id n [] 0 gl
(* Refine as a cofixpoint *)
let mutual_cofix = Tacmach.mutual_cofix
let cofix ido gl = match ido with
| None ->
- mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] gl
+ mutual_cofix (fresh_id [] (Pfedit.get_current_proof_name ()) gl) [] 0 gl
| Some id ->
- mutual_cofix id [] gl
+ mutual_cofix id [] 0 gl
(**************************************************************)
(* Reduction and conversion tactics *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index dd18aa86a..e00088dd8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -53,9 +53,9 @@ val convert_concl : constr -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val mutual_fix :
- identifier -> int -> (identifier * int * constr) list -> tactic
+ identifier -> int -> (identifier * int * constr) list -> int -> tactic
val fix : identifier option -> int -> tactic
-val mutual_cofix : identifier -> (identifier * constr) list -> tactic
+val mutual_cofix : identifier -> (identifier * constr) list -> int -> tactic
val cofix : identifier option -> tactic
(*s Introduction tactics. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 15:14:51 +0000