From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- proofs/logic.ml | 452 ++++++++++++++++++++------------------------------------ 1 file changed, 163 insertions(+), 289 deletions(-) (limited to 'proofs/logic.ml') diff --git a/proofs/logic.ml b/proofs/logic.ml index cefeb8ae..1f79d73c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml,v 1.80.2.5 2005/12/17 21:15:52 herbelin Exp $ *) +(* $Id: logic.ml 8696 2006-04-11 07:05:50Z herbelin $ *) open Pp open Util @@ -25,7 +25,6 @@ open Proof_trees open Proof_type open Typeops open Type_errors -open Coqast open Retyping open Evarutil @@ -40,114 +39,72 @@ type refiner_error = | NonLinearProof of constr (* Errors raised by the tactics *) - | CannotUnify of constr * constr - | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr | IntroNeedsProduct | DoesNotOccurIn of constr * identifier - | NoOccurrenceFound of constr exception RefinerError of refiner_error open Pretype_errors -let catchable_exception = function - | Util.UserError _ | TypeError _ | RefinerError _ - | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ | - Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) | - Indtypes.InductiveError (Indtypes.NotAllowedCaseAnalysis _ ))) -> true +let rec catchable_exception = function + | Stdpp.Exc_located(_,e) -> catchable_exception e + | Util.UserError _ | TypeError _ + | RefinerError _ | Indrec.RecursionSchemeError _ + | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _) + (* unification errors *) + | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _| + CannotUnifyBindingType _|NotClean _)) -> true | _ -> false -let error_cannot_unify (m,n) = - raise (RefinerError (CannotUnify (m,n))) - (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false - -let without_check tac gl = - let c = !check in - check := false; - try let r = tac gl in check := c; r with e -> check := c; raise e - let with_check = Options.with_option check - + (************************************************************************) (************************************************************************) (* Implementation of the structural rules (moving and deleting hypotheses around) *) -let check_clear_forward cleared_ids used_ids whatfor = - if !check && cleared_ids<>[] then - Idset.iter - (fun id' -> - if List.mem id' cleared_ids then - error (string_of_id id'^" is used in "^whatfor)) - used_ids - (* The Clear tactic: it scans the context for hypotheses to be removed (instead of iterating on the list of identifier to be removed, which forces the user to give them in order). *) let clear_hyps ids gl = let env = Global.env() in - let (nhyps,rmv) = - Sign.fold_named_context - (fun (id,c,ty as d) (hyps,rmv) -> - if List.mem id ids then - (hyps,id::rmv) - else begin - check_clear_forward rmv (global_vars_set_of_decl env d) - ("hypothesis "^string_of_id id); - (add_named_decl d hyps, rmv) - end) - gl.evar_hyps - ~init:(empty_named_context,[]) in + let (nhyps,cleared_ids) = + let fcheck cleared_ids (id,_,_ as d) = + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^ + " is used in hypothesis "^string_of_id id)) + (global_vars_set_of_decl env d) in + clear_hyps ids fcheck gl.evar_hyps in let ncl = gl.evar_concl in - check_clear_forward rmv (global_vars_set env ncl) "conclusion"; + if !check && cleared_ids<>[] then + Idset.iter + (fun id' -> + if List.mem id' cleared_ids then + error (string_of_id id'^" is used in conclusion")) + (global_vars_set env ncl); mk_goal nhyps ncl (* The ClearBody tactic *) (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and - returns [tail::(f head (id,_,_) tail)] *) + returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = - let found = ref false in - let sign' = - fold_named_context_both_sides - (fun head (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f head d tail - end else - add_named_decl d head) - sign ~init:empty_named_context - in - if (not !check) || !found then sign' else error "No such assumption" - -(* Same but with whole environment *) -let apply_to_hyp2 env id f = - let found = ref false in - let env' = - fold_named_context_both_sides - (fun env (idc,c,ct as d) tail -> - if idc = id then begin - found := true; f env d tail - end else - push_named d env) - (named_context env) ~init:(reset_context env) - in - if (not !check) || !found then env' else error "No such assumption" + try apply_to_hyp sign id f + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let apply_to_hyp_and_dependent_on sign id f g = - let found = ref false in - let sign = - Sign.fold_named_context - (fun (idc,_,_ as d) oldest -> - if idc = id then (found := true; add_named_decl (f d) oldest) - else if !found then add_named_decl (g d) oldest - else add_named_decl d oldest) - sign ~init:empty_named_context - in - if (not !check) || !found then sign else error "No such assumption" + try apply_to_hyp_and_dependent_on sign id f g + with Hyp_not_found -> + if !check then error "No such assumption" + else sign let check_typability env sigma c = if !check then let _ = type_of env sigma c in () @@ -162,26 +119,24 @@ let recheck_typability (what,id) env sigma t = ("The correctness of "^s^" relies on the body of "^(string_of_id id)) let remove_hyp_body env sigma id = - apply_to_hyp2 env id - (fun env (_,c,t) tail -> - match c with - | None -> error ((string_of_id id)^" is not a local definition") - | Some c -> - let env' = push_named (id,None,t) env in - if !check then - ignore - (Sign.fold_named_context - (fun (id',c,t as d) env'' -> - (match c with - | None -> - recheck_typability (Some id',id) env'' sigma t - | Some b -> - let b' = mkCast (b,t) in - recheck_typability (Some id',id) env'' sigma b'); - push_named d env'') - (List.rev tail) ~init:env'); - env') - + let sign = + apply_to_hyp_and_dependent_on (named_context_val env) id + (fun (_,c,t) _ -> + match c with + | None -> error ((string_of_id id)^" is not a local definition") + | Some c ->(id,None,t)) + (fun (id',c,t as d) sign -> + (if !check then + begin + let env = reset_with_named_context sign env in + match c with + | None -> recheck_typability (Some id',id) env sigma t + | Some b -> + let b' = mkCast (b,DEFAULTcast, t) in + recheck_typability (Some id',id) env sigma b' + end;d)) + in + reset_with_named_context sign env (* Auxiliary functions for primitive MOVE tactic * @@ -231,9 +186,16 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = moverec first' middle' right in if toleft then - List.rev_append (moverec [] [declfrom] left) right + let right = + List.fold_right push_named_context_val right empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right (moverec [] [declfrom] left) else - List.rev_append left (moverec [] [declfrom] right) + let right = + List.fold_right push_named_context_val + (moverec [] [declfrom] right) empty_named_context_val in + List.fold_left (fun sign d -> push_named_context_val d sign) + right left let check_backward_dependencies sign d = if not (Idset.for_all @@ -255,8 +217,8 @@ let check_forward_dependencies id tail = let rename_hyp id1 id2 sign = apply_to_hyp_and_dependent_on sign id1 - (fun (_,b,t) -> (id2,b,t)) - (map_named_declaration (replace_vars [id1,mkVar id2])) + (fun (_,b,t) _ -> (id2,b,t)) + (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d) let replace_hyp sign id d = apply_to_hyp sign id @@ -264,13 +226,17 @@ let replace_hyp sign id d = if !check then (check_backward_dependencies sign d; check_forward_dependencies id tail); - add_named_decl d sign) + d) +(* why we dont check that id does not appear in tail ??? *) let insert_after_hyp sign id d = - apply_to_hyp sign id - (fun sign d' _ -> - if !check then check_backward_dependencies sign d; - add_named_decl d (add_named_decl d' sign)) + try + insert_after_hyp sign id d + (fun sign -> + if !check then check_backward_dependencies sign d) + with Hyp_not_found -> + if !check then error "No such assumption" + else sign (************************************************************************) (************************************************************************) @@ -282,7 +248,7 @@ variables only in Application and Case *) let collect_meta_variables c = let rec collrec acc c = match kind_of_term c with | Meta mv -> mv::acc - | Cast(c,_) -> collrec acc c + | Cast(c,_,_) -> collrec acc c | (App _| Case _) -> fold_constr collrec acc c | _ -> acc in @@ -311,13 +277,17 @@ let rec mk_refgoals sigma goal goalacc conclty trm = raise (RefinerError (OccurMetaGoal conclty)); (mk_goal hyps (nf_betaiota conclty))::goalacc, conclty - | Cast (t,ty) -> + | Cast (t,_, ty) -> check_typability env sigma ty; check_conv_leq_goal env sigma trm ty conclty; mk_refgoals sigma goal goalacc ty t | App (f,l) -> - let (acc',hdty) = mk_hdgoals sigma goal goalacc f in + let (acc',hdty) = + if isInd f & not (array_exists occur_meta l) (* we could be finer *) + then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + else mk_hdgoals sigma goal goalacc f + in let (acc'',conclty') = mk_arggoals sigma goal acc' hdty (Array.to_list l) in check_conv_leq_goal env sigma trm conclty' conclty; @@ -346,12 +316,20 @@ and mk_hdgoals sigma goal goalacc trm = let env = evar_env goal in let hyps = goal.evar_hyps in match kind_of_term trm with - | Cast (c,ty) when isMeta c -> + | Cast (c,_, ty) when isMeta c -> check_typability env sigma ty; (mk_goal hyps (nf_betaiota ty))::goalacc,ty + | Cast (t,_, ty) -> + check_typability env sigma ty; + mk_refgoals sigma goal goalacc ty t + | App (f,l) -> - let (acc',hdty) = mk_hdgoals sigma goal goalacc f in + let (acc',hdty) = + if isInd f & not (array_exists occur_meta l) (* we could be finer *) + then (goalacc,type_of_applied_inductive env sigma (destInd f) l) + else mk_hdgoals sigma goal goalacc f + in mk_arggoals sigma goal acc' hdty (Array.to_list l) | Case (_,p,c,lf) -> @@ -397,16 +375,13 @@ let error_use_instantiate () = let convert_hyp sign sigma (id,b,bt as d) = apply_to_hyp sign id - (fun sign (_,c,ct) _ -> + (fun _ (_,c,ct) _ -> let env = Global.env_of_context sign in if !check && not (is_conv env sigma bt ct) then - (* Just a warning in V8.0bugfix for compatibility *) - msgnl (str "Compatibility warning: Hazardeous change of the type of " ++ pr_id id ++ - str " (not well-typed in current signature)"); + error ("Incorrect change of the type of "^(string_of_id id)); if !check && not (option_compare (is_conv env sigma) b c) then - msgnl (str "Compatibility warning: Hazardeous change of the body of " ++ pr_id id ++ - str " (not well-typed in current signature)"); - add_named_decl d sign) + error ("Incorrect change of the body of "^(string_of_id id)); + d) (************************************************************************) @@ -420,18 +395,18 @@ let prim_refiner r sigma goal = match r with (* Logical rules *) | Intro id -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; (match kind_of_term (strip_outer_cast cl) with | Prod (_,c1,b) -> if occur_meta c1 then error_use_instantiate(); - let sg = mk_goal (add_named_decl (id,None,c1) sign) + let sg = mk_goal (push_named_context_val (id,None,c1) sign) (subst1 (mkVar id) b) in [sg] | LetIn (_,c1,t1,b) -> if occur_meta c1 or occur_meta t1 then error_use_instantiate(); let sg = - mk_goal (add_named_decl (id,Some c1,t1) sign) + mk_goal (push_named_context_val (id,Some c1,t1) sign) (subst1 (mkVar id) b) in [sg] | _ -> @@ -453,11 +428,11 @@ let prim_refiner r sigma goal = raise (RefinerError IntroNeedsProduct)) | Cut (b,id,t) -> - if !check && mem_named_context id sign then + if !check && mem_named_context id (named_context_of_val sign) then error "New variable is already declared"; if occur_meta t then error_use_instantiate(); let sg1 = mk_goal sign (nf_betaiota t) in - let sg2 = mk_goal (add_named_decl (id,None,t) sign) cl in + let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in if b then [sg1;sg2] else [sg2;sg1] | FixRule (f,n,rest) -> @@ -481,9 +456,9 @@ let prim_refiner r sigma goal = if not (sp=sp') then error ("fixpoints should be on the same " ^ "mutual inductive declaration"); - if !check && mem_named_context f sign then + if !check && mem_named_context f (named_context_of_val sign) then error "name already used in the environment"; - mk_sign (add_named_decl (f,None,ar) sign) oth + mk_sign (push_named_context_val (f,None,ar) sign) oth | [] -> List.map (fun (_,_,c) -> mk_goal sign c) all in @@ -506,11 +481,11 @@ let prim_refiner r sigma goal = let rec mk_sign sign = function | (f,ar)::oth -> (try - (let _ = Sign.lookup_named f sign in + (let _ = lookup_named_val f sign in error "name already used in the environment") with | Not_found -> - mk_sign (add_named_decl (f,None,ar) sign) oth) + 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 @@ -523,7 +498,7 @@ let prim_refiner r sigma goal = sgl (* Conversion rules *) - | Convert_concl cl' -> + | Convert_concl (cl',_) -> check_typability env sigma cl'; if (not !check) || is_conv_leq env sigma cl' cl then let sg = mk_goal sign cl' in @@ -544,18 +519,20 @@ let prim_refiner r sigma goal = if !check then recheck_typability (None,id) env' sigma cl; env' in - let sign' = named_context (List.fold_left clear_aux env ids) in + let sign' = named_context_val (List.fold_left clear_aux env ids) in let sg = mk_goal sign' cl in [sg] | Move (withdep, hfrom, hto) -> - let (left,right,declfrom,toleft) = split_sign hfrom hto sign in + let (left,right,declfrom,toleft) = + split_sign hfrom hto (named_context_of_val sign) in let hyps' = move_after withdep toleft (left,declfrom,right) hto in [mk_goal hyps' cl] | Rename (id1,id2) -> - if !check & id1 <> id2 & List.mem id2 (ids_of_named_context sign) then + if !check & id1 <> id2 && + List.mem id2 (ids_of_named_context (named_context_of_val sign)) then error ((string_of_id id2)^" is already used"); let sign' = rename_hyp id1 id2 sign in let cl' = replace_vars [id1,mkVar id2] cl in @@ -566,15 +543,39 @@ let prim_refiner r sigma goal = (* Extracting a proof term from the proof tree *) (* Util *) + +type variable_proof_status = ProofVar | SectionVar of identifier + +type proof_variable = name * variable_proof_status + +let subst_proof_vars = + let rec aux p vars = + let _,subst = + List.fold_left (fun (n,l) var -> + let t = match var with + | Anonymous,_ -> l + | Name id, ProofVar -> (id,mkRel n)::l + | Name id, SectionVar id' -> (id,mkVar id')::l in + (n+1,t)) (p,[]) vars + in replace_vars (List.rev subst) + in aux 1 + let rec rebind id1 id2 = function - | [] -> [] - | id::l -> - if id = id1 then id2::l else + | [] -> [Name id2,SectionVar id1] + | (na,_ as x)::l -> + if na = Name id1 then (Name id2,ProofVar)::l else let l' = rebind id1 id2 l in - if id = id2 then - (* TODO: find a more elegant way to hide a variable *) - (id_of_string "_@")::l' - else id::l' + if na = Name id2 then (Anonymous,ProofVar)::l' else x::l' + +let add_proof_var id vl = (Name id,ProofVar)::vl + +let proof_variable_index x = + let rec aux n = function + | (Name id,ProofVar)::l when x = id -> n + | _::l -> aux (n+1) l + | [] -> raise Not_found + in + aux 1 let prim_extractor subfun vl pft = let cl = pft.goal.evar_concl in @@ -582,61 +583,64 @@ let prim_extractor subfun vl pft = | Some (Prim (Intro id), [spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Intro_replacing id),[spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Cut (b,id,t)),[spf1;spf2]) -> let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in - mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2) + 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 - let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all 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,_,_)->(id::vl)) (f::vl)others 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)) | Some (Prim (Cofix (f,others)),spfl) -> let all = Array.of_list ((f,cl)::others) in - let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all 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,_)->(id::vl)) (f::vl) others 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)) | Some (Prim (Refine c),spfl) -> let mvl = collect_meta_variables c in let metamap = List.combine mvl (List.map (subfun vl) spfl) in - let cc = subst_vars vl c in + let cc = subst_proof_vars vl c in plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) - | Some (Prim (Convert_concl _),[pf]) -> - subfun vl pf - + | Some (Prim (Convert_concl (t,k)),[pf]) -> + if k = DEFAULTcast then subfun vl pf + else mkCast (subfun vl pf,k,subst_proof_vars vl cl) | Some (Prim (Convert_hyp _),[pf]) -> subfun vl pf | Some (Prim (Thin _),[pf]) -> - (* No need to make ids Anonymous in vl: subst_vars take the more recent *) + (* No need to make ids Anon in vl: subst_proof_vars take the most recent*) subfun vl pf | Some (Prim (ThinBody _),[pf]) -> @@ -652,133 +656,3 @@ let prim_extractor subfun vl pft = | None-> error "prim_extractor handed incomplete proof" -(* Pretty-printer *) - -open Printer - -let prterm x = prterm_env (Global.env()) x - -let pr_prim_rule_v7 = function - | Intro id -> - str"Intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"Assert " ++ prterm t) - else - (str"Cut " ++ prterm t ++ str ";[Intro " ++ pr_id id ++ str "|Idtac]") - - | FixRule (f,n,[]) -> - (str"Fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"Fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"Cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth) - | [] -> mt () in - (str"Cofix " ++ pr_id f ++ str" with " ++ print_mut others) - - | Refine c -> - str(if occur_meta c then "Refine " else "Exact ") ++ - Constrextern.with_meta_as_hole prterm c - - | Convert_concl c -> - (str"Change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"Change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"Change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (Type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"Clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"ClearBody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "Dependent " else "") ++ - str"Move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "Rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule_v8 = function - | Intro id -> - str"intro " ++ pr_id id - - | Intro_replacing id -> - (str"intro replacing " ++ pr_id id) - - | Cut (b,id,t) -> - if b then - (str"assert " ++ prterm t) - else - (str"cut " ++ prterm t ++ str ";[intro " ++ pr_id id ++ str "|idtac]") - - | FixRule (f,n,[]) -> - (str"fix " ++ pr_id f ++ str"/" ++ int n) - - | FixRule (f,n,others) -> - let rec print_mut = function - | (f,n,ar)::oth -> - pr_id f ++ str"/" ++ int n ++ str" : " ++ prterm ar ++ print_mut oth - | [] -> mt () in - (str"fix " ++ pr_id f ++ str"/" ++ int n ++ - str" with " ++ print_mut others) - - | Cofix (f,[]) -> - (str"cofix " ++ pr_id f) - - | Cofix (f,others) -> - let rec print_mut = function - | (f,ar)::oth -> - (pr_id f ++ str" : " ++ prterm ar ++ print_mut oth) - | [] -> mt () in - (str"cofix " ++ pr_id f ++ str" with " ++ print_mut others) - - | Refine c -> - str(if occur_meta c then "refine " else "exact ") ++ - Constrextern.with_meta_as_hole prterm c - - | Convert_concl c -> - (str"change " ++ prterm c) - - | Convert_hyp (id,None,t) -> - (str"change " ++ prterm t ++ spc () ++ str"in " ++ pr_id id) - - | Convert_hyp (id,Some c,t) -> - (str"change " ++ prterm c ++ spc () ++ str"in " - ++ pr_id id ++ str" (type of " ++ pr_id id ++ str ")") - - | Thin ids -> - (str"clear " ++ prlist_with_sep pr_spc pr_id ids) - - | ThinBody ids -> - (str"clearbody " ++ prlist_with_sep pr_spc pr_id ids) - - | Move (withdep,id1,id2) -> - (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ str " after " ++ pr_id id2) - - | Rename (id1,id2) -> - (str "rename " ++ pr_id id1 ++ str " into " ++ pr_id id2) - -let pr_prim_rule t = - if! Options.v7 then pr_prim_rule_v7 t else pr_prim_rule_v8 t -- cgit v1.2.3