diff options
author | 2009-09-17 15:58:14 +0000 | |
---|---|---|
committer | 2009-09-17 15:58:14 +0000 | |
commit | 61ccbc81a2f3b4662ed4a2bad9d07d2003dda3a2 (patch) | |
tree | 961cc88c714aa91a0276ea9fbf8bc53b2b9d5c28 /toplevel/auto_ind_decl.ml | |
parent | 6d3fbdf36c6a47b49c2a4b16f498972c93c07574 (diff) |
Delete trailing whitespaces in all *.{v,ml*} files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r-- | toplevel/auto_ind_decl.ml | 390 |
1 files changed, 195 insertions, 195 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 5ddf2b705..3e025b032 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -30,7 +30,7 @@ open Ind_tables (* boolean equality *) -let quick_chop n l = +let quick_chop n l = let rec kick_last = function | t::[] -> [] | t::q -> t::(kick_last q) @@ -39,20 +39,20 @@ and aux = function | (0,l') -> l' | (n,h::t) -> aux (n-1,t) | _ -> failwith "quick_chop" - in + in if n > (List.length l) then failwith "quick_chop args" else kick_last (aux (n,l) ) -let rec deconstruct_type t = +let rec deconstruct_type t = let l,r = decompose_prod t in (List.map (fun (_,b) -> b) (List.rev l))@[r] -let subst_in_constr (_,subst,(ind,const)) = +let subst_in_constr (_,subst,(ind,const)) = let ind' = (subst_kn subst (fst ind)),(snd ind) and const' = subst_mps subst const in ind',const' -exception EqNotFound of string +exception EqNotFound of string exception EqUnknown of string let dl = dummy_loc @@ -62,28 +62,28 @@ let bb = constr_of_global Coqlib.glob_bool let andb_prop = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb_prop -let andb_true_intro = fun _ -> - (Coqlib.build_bool_type()).Coqlib.andb_true_intro +let andb_true_intro = fun _ -> + (Coqlib.build_bool_type()).Coqlib.andb_true_intro -let tt = constr_of_global Coqlib.glob_true +let tt = constr_of_global Coqlib.glob_true let ff = constr_of_global Coqlib.glob_false -let eq = constr_of_global Coqlib.glob_eq +let eq = constr_of_global Coqlib.glob_eq -let sumbool = Coqlib.build_coq_sumbool +let sumbool = Coqlib.build_coq_sumbool -let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb (* reconstruct the inductive with the correct deBruijn indexes *) -let mkFullInd ind n = +let mkFullInd ind n = let mib = Global.lookup_mind (fst ind) in let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in (* params context divided *) - let lnonparrec,lnamesparrec = + let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in - if nparrec > 0 + if nparrec > 0 then mkApp (mkInd ind, Array.of_list(extended_rel_list (nparrec+n) lnamesparrec)) else mkInd ind @@ -99,33 +99,33 @@ let make_eq_scheme sp = let nparams = mib.mind_nparams in let nparrec = mib.mind_nparams_rec in (* params context divided *) - let lnonparrec,lnamesparrec = + let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in (* predef coq's boolean type *) (* rec name *) let rec_name i =(string_of_id (Array.get mib.mind_packets i).mind_typename)^ - "_eqrec" + "_eqrec" in (* construct the "fun A B ... N, eqA eqB eqC ... N => fixpoint" part *) let create_input c = - let myArrow u v = mkArrow u (lift 1 v) + let myArrow u v = mkArrow u (lift 1 v) and eqName = function | Name s -> id_of_string ("eq_"^(string_of_id s)) - | Anonymous -> id_of_string "eq_A" + | Anonymous -> id_of_string "eq_A" in let ext_rel_list = extended_rel_list 0 lnamesparrec in let lift_cnt = ref 0 in - let eqs_typ = List.map (fun aa -> - let a = lift !lift_cnt aa in - incr lift_cnt; - myArrow a (myArrow a bb) + let eqs_typ = List.map (fun aa -> + let a = lift !lift_cnt aa in + incr lift_cnt; + myArrow a (myArrow a bb) ) ext_rel_list in let eq_input = List.fold_left2 ( fun a b (n,_,_) -> (* mkLambda(n,b,a) ) *) (* here I leave the Naming thingy so that the type of the function is more readable for the user *) - mkNamedLambda (eqName n) b a ) + mkNamedLambda (eqName n) b a ) c (List.rev eqs_typ) lnamesparrec in List.fold_left (fun a (n,_,t) ->(* mkLambda(n,t,a)) eq_input rel_list *) @@ -134,83 +134,83 @@ let make_eq_scheme sp = (match n with Name s -> s | Anonymous -> id_of_string "A") t a) eq_input lnamesparrec in - let make_one_eq cur = - let ind = sp,cur in + let make_one_eq cur = + let ind = sp,cur in (* current inductive we are working on *) - let cur_packet = mib.mind_packets.(snd ind) in + let cur_packet = mib.mind_packets.(snd ind) in (* Inductive toto : [rettyp] := *) let rettyp = Inductive.type_of_inductive env (mib,cur_packet) in - (* split rettyp in a list without the non rec params and the last -> + (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in (* give a type A, this function tries to find the equality on A declared previously *) (* nlist = the number of args (A , B , ... ) eqA = the deBruijn index of the first eq param - ndx = how much to translate due to the 2nd Case + ndx = how much to translate due to the 2nd Case *) - let compute_A_equality rel_list nlist eqA ndx t = + let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in let rec aux c a = match c with | Rel x -> mkRel (x-nlist+ndx) - | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))) - | Cast (x,_,_) -> aux (kind_of_term x) a - | App (x,newa) -> aux (kind_of_term x) newa + | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))) + | Cast (x,_,_) -> aux (kind_of_term x) a + | App (x,newa) -> aux (kind_of_term x) newa | Ind (sp',i) -> if sp=sp' then mkRel(eqA-nlist-i+nb_ind-1) - else ( try - let eq = find_eq_scheme (sp',i) - and eqa = Array.map - (fun x -> aux (kind_of_term x) [||] ) a + else ( try + let eq = find_eq_scheme (sp',i) + and eqa = Array.map + (fun x -> aux (kind_of_term x) [||] ) a in - let args = Array.append - (Array.map (fun x->lift lifti x) a) eqa - in if args = [||] then eq - else mkApp (eq,Array.append + let args = Array.append + (Array.map (fun x->lift lifti x) a) eqa + in if args = [||] then eq + else mkApp (eq,Array.append (Array.map (fun x->lift lifti x) a) eqa) with Not_found -> raise(EqNotFound (string_of_kn sp')) ) | Sort _ -> raise (EqUnknown "Sort" ) | Prod _ -> raise (EqUnknown "Prod" ) - | Lambda _-> raise (EqUnknown "Lambda") + | Lambda _-> raise (EqUnknown "Lambda") | LetIn _ -> raise (EqUnknown "LetIn") - | Const kn -> let mp,dir,lbl= repr_con kn in + | Const kn -> let mp,dir,lbl= repr_con kn in mkConst (make_con mp dir ( - mk_label ("eq_"^(string_of_label lbl)))) + mk_label ("eq_"^(string_of_label lbl)))) | Construct _ -> raise (EqUnknown "Construct") | Case _ -> raise (EqUnknown "Case") | CoFix _ -> raise (EqUnknown "CoFix") - | Fix _ -> raise (EqUnknown "Fix") - | Meta _ -> raise (EqUnknown "Meta") + | Fix _ -> raise (EqUnknown "Fix") + | Meta _ -> raise (EqUnknown "Meta") | Evar _ -> raise (EqUnknown "Evar") in aux t [||] in (* construct the predicate for the Case part*) - let do_predicate rel_list n = - List.fold_left (fun a b -> mkLambda(Anonymous,b,a)) + let do_predicate rel_list n = + List.fold_left (fun a b -> mkLambda(Anonymous,b,a)) (mkLambda (Anonymous, mkFullInd ind (n+3+(List.length rettyp_l)+nb_ind-1), - bb)) - (List.rev rettyp_l) in + bb)) + (List.rev rettyp_l) in (* make_one_eq *) - (* do the [| C1 ... => match Y with ... end - ... + (* do the [| C1 ... => match Y with ... end + ... Cn => match Y with ... end |] part *) let ci = make_case_info env ind MatchStyle in let constrs n = get_constructors env (make_ind_family (ind, extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in let constrsi = constrs (3+nparrec) in let n = Array.length constrsi in - let ar = Array.create n ff in + let ar = Array.create n ff in for i=0 to n-1 do let nb_cstr_args = List.length constrsi.(i).cs_args in let ar2 = Array.create n ff in let constrsj = constrs (3+nparrec+nb_cstr_args) in for j=0 to n-1 do - if (i=j) then + if (i=j) then ar2.(j) <- let cc = (match nb_cstr_args with | 0 -> tt - | _ -> let eqs = Array.make nb_cstr_args tt in + | _ -> let eqs = Array.make nb_cstr_args tt in for ndx = 0 to nb_cstr_args-1 do let _,_,cc = List.nth constrsi.(i).cs_args ndx in let eqA = compute_A_equality rel_list @@ -218,53 +218,53 @@ let make_eq_scheme sp = (nparrec+3+2*nb_cstr_args) (nb_cstr_args+ndx+1) (kind_of_term cc) - in - Array.set eqs ndx + in + Array.set eqs ndx (mkApp (eqA, [|mkRel (ndx+1+nb_cstr_args);mkRel (ndx+1)|] )) - done; - Array.fold_left - (fun a b -> mkApp (andb(),[|b;a|])) - (eqs.(0)) + done; + Array.fold_left + (fun a b -> mkApp (andb(),[|b;a|])) + (eqs.(0)) (Array.sub eqs 1 (nb_cstr_args - 1)) ) in (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) cc - (constrsj.(j).cs_args) - ) + (constrsj.(j).cs_args) + ) else ar2.(j) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) ff (constrsj.(j).cs_args) ) done; - ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) + ar.(i) <- (List.fold_left (fun a (p,q,r) -> mkLambda (p,r,a)) (mkCase (ci,do_predicate rel_list nb_cstr_args, mkVar (id_of_string "Y") ,ar2)) - (constrsi.(i).cs_args)) + (constrsi.(i).cs_args)) done; mkNamedLambda (id_of_string "X") (mkFullInd ind (nb_ind-1+1)) ( mkNamedLambda (id_of_string "Y") (mkFullInd ind (nb_ind-1+2)) ( - mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar))) + mkCase (ci, do_predicate rel_list 0,mkVar (id_of_string "X"),ar))) in (* make_eq_scheme *) try - let names = Array.make nb_ind Anonymous and - types = Array.make nb_ind mkSet and + let names = Array.make nb_ind Anonymous and + types = Array.make nb_ind mkSet and cores = Array.make nb_ind mkSet and - res = Array.make nb_ind mkSet in + res = Array.make nb_ind mkSet in for i=0 to (nb_ind-1) do names.(i) <- Name (id_of_string (rec_name i)); - types.(i) <- mkArrow (mkFullInd (sp,i) 0) + types.(i) <- mkArrow (mkFullInd (sp,i) 0) (mkArrow (mkFullInd (sp,i) 1) bb); cores.(i) <- make_one_eq i - done; - if (string_of_mp (modpath sp ))="Coq.Init.Logic" + done; + if (string_of_mp (modpath sp ))="Coq.Init.Logic" then print_string "Logic time, do nothing.\n" else ( - for i=0 to (nb_ind-1) do + for i=0 to (nb_ind-1) do let cpack = Array.get mib.mind_packets i in if check_eq_scheme (sp,i) then message ("Boolean equality is already defined on "^ - (string_of_id cpack.mind_typename)^".") + (string_of_id cpack.mind_typename)^".") else ( let fix = mkFix (((Array.make nb_ind 0),i),(names,types,cores)) in res.(i) <- create_input fix @@ -272,7 +272,7 @@ let make_eq_scheme sp = done; ); res - with + with | EqUnknown s -> error ("Type unexpected ("^s^ ") during boolean eq computation, please report.") | EqNotFound s -> error ("Boolean equality on "^s^ @@ -283,32 +283,32 @@ let make_eq_scheme sp = (* This function tryies to get the [inductive] between a constr the constr should be Ind i or App(Ind i,[|args|]) *) -let destruct_ind c = +let destruct_ind c = try let u,v = destApp c in let indc = destInd u in indc,v with _-> let indc = destInd c in indc,[||] -(* - In the followind, avoid is the list of names to avoid. +(* + In the followind, avoid is the list of names to avoid. If the args of the Inductive type are A1 ... An - then avoid should be + then avoid should be [| lb_An ... lb _A1 (resp. bl_An ... bl_A1) eq_An .... eq_A1 An ... A1 |] so from Ai we can find the the correct eq_Ai bl_ai or lb_ai *) (* used in the leib -> bool side*) -let do_replace_lb aavoid narg gls p q = +let do_replace_lb aavoid narg gls p q = let avoid = Array.of_list aavoid in - let do_arg v offset = - try + let do_arg v offset = + try let x = narg*offset in - let s = destVar v in + let s = destVar v in let n = Array.length avoid in - let rec find i = - if avoid.(n-i) = s then avoid.(n-i-x) - else (if i<n then find (i+1) + let rec find i = + if avoid.(n-i) = s then avoid.(n-i-x) + else (if i<n then find (i+1) else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) @@ -317,47 +317,47 @@ let do_replace_lb aavoid narg gls p q = ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( - if offset=1 then ("eq_"^(string_of_label lbl)) + if offset=1 then ("eq_"^(string_of_label lbl)) else ((string_of_label lbl)^"_lb") ))) ) in let type_of_pq = pf_type_of gls p in let u,v = destruct_ind type_of_pq - in let lb_type_of_p = - try find_lb_proof u - with Not_found -> + in let lb_type_of_p = + try find_lb_proof u + with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = msg_with Format.str_formatter (str "Leibniz->boolean:" ++ - str "You have to declare the" ++ + str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr type_of_pq ++ + Printer.pr_constr type_of_pq ++ str " first."); Format.flush_str_formatter () in error err_msg - in let lb_args = Array.append (Array.append + in let lb_args = Array.append (Array.append (Array.map (fun x -> x) v) (Array.map (fun x -> do_arg x 1) v)) (Array.map (fun x -> do_arg x 2) v) - in let app = if lb_args = [||] - then lb_type_of_p else mkApp (lb_type_of_p,lb_args) + in let app = if lb_args = [||] + then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in [Equality.replace p q ; apply app ; Auto.default_auto] (* used in the bool -> leib side *) -let do_replace_bl ind gls aavoid narg lft rgt = - let avoid = Array.of_list aavoid in - let do_arg v offset = - try +let do_replace_bl ind gls aavoid narg lft rgt = + let avoid = Array.of_list aavoid in + let do_arg v offset = + try let x = narg*offset in - let s = destVar v in + let s = destVar v in let n = Array.length avoid in - let rec find i = - if avoid.(n-i) = s then avoid.(n-i-x) - else (if i<n then find (i+1) + let rec find i = + if avoid.(n-i) = s then avoid.(n-i-x) + else (if i<n then find (i+1) else error ("Var "^(string_of_id s)^" seems unknown.") ) in mkVar (find 1) @@ -366,60 +366,60 @@ let do_replace_bl ind gls aavoid narg lft rgt = ( let mp,dir,lbl = repr_con (destConst v) in mkConst (make_con mp dir (mk_label ( - if offset=1 then ("eq_"^(string_of_label lbl)) + if offset=1 then ("eq_"^(string_of_label lbl)) else ((string_of_label lbl)^"_bl") ))) ) in - let rec aux l1 l2 = + let rec aux l1 l2 = match (l1,l2) with | (t1::q1,t2::q2) -> let tt1 = pf_type_of gls t1 in if t1=t2 then aux q1 q2 else ( - let u,v = try destruct_ind tt1 + let u,v = try destruct_ind tt1 (* trick so that the good sequence is returned*) with _ -> ind,[||] - in if u = ind + in if u = ind then (Equality.replace t1 t2)::(Auto.default_auto)::(aux q1 q2) else ( - let bl_t1 = - try find_bl_proof u - with Not_found -> + let bl_t1 = + try find_bl_proof u + with Not_found -> (* spiwack: the format of this error message should probably be improved. *) - let err_msg = msg_with Format.str_formatter + let err_msg = msg_with Format.str_formatter (str "boolean->Leibniz:" ++ - str "You have to declare the" ++ + str "You have to declare the" ++ str "decidability over " ++ - Printer.pr_constr tt1 ++ + Printer.pr_constr tt1 ++ str " first."); Format.flush_str_formatter () in error err_msg - in let bl_args = - Array.append (Array.append + in let bl_args = + Array.append (Array.append (Array.map (fun x -> x) v) (Array.map (fun x -> do_arg x 1) v)) (Array.map (fun x -> do_arg x 2) v ) - in - let app = if bl_args = [||] - then bl_t1 else mkApp (bl_t1,bl_args) - in - (Equality.replace_by t1 t2 + in + let app = if bl_args = [||] + then bl_t1 else mkApp (bl_t1,bl_args) + in + (Equality.replace_by t1 t2 (tclTHEN (apply app) (Auto.default_auto)))::(aux q1 q2) ) ) | ([],[]) -> [] | _ -> error "Both side of the equality must have the same arity." in - let (ind1,ca1) = try destApp lft with + let (ind1,ca1) = try destApp lft with _ -> error "replace failed." and (ind2,ca2) = try destApp rgt with _ -> error "replace failed." in let (sp1,i1) = try destInd ind1 with - _ -> (try fst (destConstruct ind1) with _ -> + _ -> (try fst (destConstruct ind1) with _ -> error "The expected type is an inductive one.") and (sp2,i2) = try destInd ind2 with _ -> (try fst (destConstruct ind2) with _ -> @@ -427,14 +427,14 @@ let do_replace_bl ind gls aavoid narg lft rgt = in if (sp1 <> sp2) || (i1 <> i2) then (error "Eq should be on the same type") - else (aux (Array.to_list ca1) (Array.to_list ca2)) + else (aux (Array.to_list ca1) (Array.to_list ca2)) -(* +(* create, from a list of ids [i1,i2,...,in] the list [(in,eq_in,in_bl,in_al),,...,(i1,eq_i1,i1_bl_i1_al )] *) -let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = - match n with +let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = + match n with Name s -> string_of_id s | Anonymous -> "A" in (id_of_string s',id_of_string ("eq_"^s'), @@ -445,61 +445,61 @@ let list_id l = List.fold_left ( fun a (n,_,t) -> let s' = (* build the right eq_I A B.. N eq_A .. eq_N *) -let eqI ind l = +let eqI ind l = let list_id = list_id l in let eA = Array.of_list((List.map (fun (s,_,_,_) -> mkVar s) list_id)@ (List.map (fun (_,seq,_,_)-> mkVar seq) list_id )) - and e = try find_eq_scheme ind with - Not_found -> error + and e = try find_eq_scheme ind with + Not_found -> error ("The boolean equality on "^(string_of_kn (fst ind))^" is needed."); in (if eA = [||] then e else mkApp(e,eA)) -let compute_bl_goal ind lnamesparrec nparrec = +let compute_bl_goal ind lnamesparrec nparrec = let eqI = eqI ind lnamesparrec in - let list_id = list_id lnamesparrec in + let list_id = list_id lnamesparrec in let create_input c = let x = id_of_string "x" and y = id_of_string "y" in let bl_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) )) - ) list_id in + ) list_id in let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> mkNamedProd sbl b a - ) c (List.rev list_id) (List.rev bl_typ) in + ) c (List.rev list_id) (List.rev bl_typ) in let eqs_typ = List.map (fun (s,_,_,_) -> mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) ) list_id in let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a - ) bl_input (List.rev list_id) (List.rev eqs_typ) in + ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a (n,_,t) -> mkNamedProd (match n with Name s -> s | Anonymous -> id_of_string "A") t a) eq_input lnamesparrec - in + in let n = id_of_string "n" and m = id_of_string "m" in create_input ( mkNamedProd n (mkFullInd ind nparrec) ( mkNamedProd m (mkFullInd ind (nparrec+1)) ( - mkArrow + mkArrow (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) (mkApp(eq,[|mkFullInd ind (nparrec+3);mkVar n;mkVar m|])) ))) - -let compute_bl_tact ind lnamesparrec nparrec = + +let compute_bl_tact ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in - let first_intros = + let first_intros = ( List.map (fun (s,_,_,_) -> s ) list_id ) @ ( List.map (fun (_,seq,_,_ ) -> seq) list_id ) @ - ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) - in + ( List.map (fun (_,_,sbl,_ ) -> sbl) list_id ) + in let fresh_first_intros = List.map ( fun s -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh ) first_intros in @@ -526,7 +526,7 @@ let compute_bl_tact ind lnamesparrec nparrec = None; intro_using freshz; intros; - tclTRY ( + tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); simpl_in_hyp (freshz,InHyp); @@ -537,9 +537,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). tclTHENSEQ [ simple_apply_in freshz (andb_prop()); fun gl -> - let fresht = fresh_id (!avoid) (id_of_string "Z") gsig + let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in - avoid := fresht::(!avoid); + avoid := fresht::(!avoid); (new_destruct false [Tacexpr.ElimOnConstr ((mkVar freshz,Rawterm.NoBindings))] None @@ -548,30 +548,30 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). dl,Genarg.IntroIdentifier freshz]])) None) gl ]); (* - Ci a1 ... an = Ci b1 ... bn + Ci a1 ... an = Ci b1 ... bn replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto *) fun gls-> let gl = (gls.Evd.it).Evd.evar_concl in match (kind_of_term gl) with - | App (c,ca) -> ( + | App (c,ca) -> ( match (kind_of_term c) with - | Ind (i1,i2) -> + | Ind (i1,i2) -> if(string_of_label (label i1) = "eq") then ( tclTHENSEQ ((do_replace_bl ind gls (!avoid) nparrec (ca.(2)) (ca.(1)))@[Auto.default_auto]) gls ) - else + else (error "Failure while solving Boolean->Leibniz.") | _ -> error "Failure while solving Boolean->Leibniz." ) | _ -> error "Failure while solving Boolean->Leibniz." - + ] ) -let compute_lb_goal ind lnamesparrec nparrec = +let compute_lb_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eqI = eqI ind lnamesparrec in let create_input c = @@ -580,43 +580,43 @@ let compute_lb_goal ind lnamesparrec nparrec = let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) )) - ) list_id in + ) list_id in let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> mkNamedProd slb b a - ) c (List.rev list_id) (List.rev lb_typ) in + ) c (List.rev list_id) (List.rev lb_typ) in let eqs_typ = List.map (fun (s,_,_,_) -> mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) ) list_id in let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a - ) lb_input (List.rev list_id) (List.rev eqs_typ) in + ) lb_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a (n,_,t) -> mkNamedProd (match n with Name s -> s | Anonymous -> id_of_string "A") t a) eq_input lnamesparrec - in + in let n = id_of_string "n" and m = id_of_string "m" in create_input ( mkNamedProd n (mkFullInd ind nparrec) ( mkNamedProd m (mkFullInd ind (nparrec+1)) ( - mkArrow + mkArrow (mkApp(eq,[|mkFullInd ind (nparrec+2);mkVar n;mkVar m|])) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar n;mkVar m|]);tt|])) ))) -let compute_lb_tact ind lnamesparrec nparrec = +let compute_lb_tact ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let avoid = ref [] in let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in - let first_intros = + let first_intros = ( List.map (fun (s,_,_,_) -> s ) list_id ) @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in let fresh_first_intros = List.map ( fun s -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh ) first_intros in @@ -630,20 +630,20 @@ let compute_lb_tact ind lnamesparrec nparrec = Pfedit.by ( tclTHENSEQ [ intros_using fresh_first_intros; intro_using freshn ; - new_induct false [Tacexpr.ElimOnConstr - ((mkVar freshn),Rawterm.NoBindings)] + new_induct false [Tacexpr.ElimOnConstr + ((mkVar freshn),Rawterm.NoBindings)] None (None,None) None; intro_using freshm; - new_destruct false [Tacexpr.ElimOnConstr + new_destruct false [Tacexpr.ElimOnConstr ((mkVar freshm),Rawterm.NoBindings)] None (None,None) None; intro_using freshz; intros; - tclTRY ( + tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); @@ -657,21 +657,21 @@ let compute_lb_tact ind lnamesparrec nparrec = (* assume the goal to be eq (eq_type ...) = true *) match (kind_of_term gl) with | App(c,ca) -> (match (kind_of_term ca.(1)) with - | App(c',ca') -> + | App(c',ca') -> let n = Array.length ca' in - tclTHENSEQ (do_replace_lb (!avoid) - nparrec gls + tclTHENSEQ (do_replace_lb (!avoid) + nparrec gls ca'.(n-2) ca'.(n-1)) gls - | _ -> error - "Failure while solving Leibniz->Boolean." + | _ -> error + "Failure while solving Leibniz->Boolean." ) - | _ -> error - "Failure while solving Leibniz->Boolean." + | _ -> error + "Failure while solving Leibniz->Boolean." ] ) (* {n=m}+{n<>m} part *) -let compute_dec_goal ind lnamesparrec nparrec = +let compute_dec_goal ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let create_input c = let x = id_of_string "x" and @@ -679,37 +679,37 @@ let compute_dec_goal ind lnamesparrec nparrec = let lb_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) )) - ) list_id in + ) list_id in let bl_typ = List.map (fun (s,seq,_,_) -> mkNamedProd x (mkVar s) ( mkNamedProd y (mkVar s) ( - mkArrow + mkArrow ( mkApp(eq,[|bb;mkApp(mkVar seq,[|mkVar x;mkVar y|]);tt|])) ( mkApp(eq,[|mkVar s;mkVar x;mkVar y|])) )) - ) list_id in + ) list_id in let lb_input = List.fold_left2 ( fun a (s,_,_,slb) b -> mkNamedProd slb b a - ) c (List.rev list_id) (List.rev lb_typ) in + ) c (List.rev list_id) (List.rev lb_typ) in let bl_input = List.fold_left2 ( fun a (s,_,sbl,_) b -> mkNamedProd sbl b a - ) lb_input (List.rev list_id) (List.rev bl_typ) in + ) lb_input (List.rev list_id) (List.rev bl_typ) in let eqs_typ = List.map (fun (s,_,_,_) -> mkProd(Anonymous,mkVar s,mkProd(Anonymous,mkVar s,bb)) ) list_id in let eq_input = List.fold_left2 ( fun a (s,seq,_,_) b -> mkNamedProd seq b a - ) bl_input (List.rev list_id) (List.rev eqs_typ) in + ) bl_input (List.rev list_id) (List.rev eqs_typ) in List.fold_left (fun a (n,_,t) -> mkNamedProd (match n with Name s -> s | Anonymous -> id_of_string "A") t a) eq_input lnamesparrec - in + in let n = id_of_string "n" and m = id_of_string "m" in let eqnm = mkApp(eq,[|mkFullInd ind (2*nparrec+2);mkVar n;mkVar m|]) in @@ -721,26 +721,26 @@ let compute_dec_goal ind lnamesparrec nparrec = ) ) -let compute_dec_tact ind lnamesparrec nparrec = +let compute_dec_tact ind lnamesparrec nparrec = let list_id = list_id lnamesparrec in let eqI = eqI ind lnamesparrec in let avoid = ref [] in let gsig = top_goal_of_pftreestate (Pfedit.get_pftreestate()) in let eqtrue x = mkApp(eq,[|bb;x;tt|]) in let eqfalse x = mkApp(eq,[|bb;x;ff|]) in - let first_intros = + let first_intros = ( List.map (fun (s,_,_,_) -> s ) list_id ) @ ( List.map (fun (_,seq,_,_) -> seq) list_id ) @ ( List.map (fun (_,_,sbl,_) -> sbl) list_id ) @ - ( List.map (fun (_,_,_,slb) -> slb) list_id ) - in + ( List.map (fun (_,_,_,slb) -> slb) list_id ) + in let fresh_first_intros = List.map ( fun s -> let fresh = fresh_id (!avoid) s gsig in avoid := fresh::(!avoid); fresh ) first_intros in let freshn = fresh_id (!avoid) (id_of_string "n") gsig in let freshm = avoid := freshn::(!avoid); fresh_id (!avoid) (id_of_string "m") gsig in - let freshH = avoid := freshm::(!avoid); + let freshH = avoid := freshm::(!avoid); fresh_id (!avoid) (id_of_string "H") gsig in let eqbnm = mkApp(eqI,[|mkVar freshn;mkVar freshm|]) in avoid := freshH::(!avoid); @@ -749,9 +749,9 @@ let compute_dec_tact ind lnamesparrec nparrec = intros_using [freshn;freshm]; assert_tac (Name freshH) ( mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) - ) ]); + ) ]); (*we do this so we don't have to prove the same goal twice *) - Pfedit.by ( tclTHEN + Pfedit.by ( tclTHEN (new_destruct false [Tacexpr.ElimOnConstr (eqbnm,Rawterm.NoBindings)] None @@ -762,8 +762,8 @@ let compute_dec_tact ind lnamesparrec nparrec = Pfedit.by ( let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in avoid := freshH2::(!avoid); - new_destruct false [Tacexpr.ElimOnConstr - ((mkVar freshH),Rawterm.NoBindings)] + new_destruct false [Tacexpr.ElimOnConstr + ((mkVar freshH),Rawterm.NoBindings)] None (None,Some (dl,Genarg.IntroOrAndPattern [ [dl,Genarg.IntroAnonymous]; @@ -782,7 +782,7 @@ let compute_dec_tact ind lnamesparrec nparrec = " equality is required.") in - (* left *) + (* left *) Pfedit.by ( tclTHENSEQ [ simplest_left; apply (mkApp(blI,Array.map(fun x->mkVar x) xargs)); Auto.default_auto @@ -794,20 +794,20 @@ let compute_dec_tact ind lnamesparrec nparrec = unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all; - assert_tac (Name freshH3) + assert_tac (Name freshH3) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) ]); - Pfedit.by + Pfedit.by (tclTHENSEQ [apply (mkApp(lbI,Array.map (fun x->mkVar x) xargs)); Auto.default_auto ]); Pfedit.by (Equality.general_rewrite_bindings_in true all_occurrences - (List.hd !avoid) + (List.hd !avoid) ((mkVar (List.hd (List.tl !avoid))), Rawterm.NoBindings ) true); Pfedit.by (Equality.discr_tac false None) - + |