From 99f4c55d9b9eb1130bff54a1ff9028b442141231 Mon Sep 17 00:00:00 2001 From: bgregoir Date: Fri, 15 Dec 2006 15:30:59 +0000 Subject: Changement dans ring et field, beaucoup de correction d'erreurs, maintenant les differentes tactics marchent mieux mais le code est moche ... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9454 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/setoid_ring/newring.ml4 | 106 +++++++++++++++++++++++----------------- 1 file changed, 62 insertions(+), 44 deletions(-) (limited to 'contrib/setoid_ring/newring.ml4') diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4 index c22f1eb17..5140b3bf0 100644 --- a/contrib/setoid_ring/newring.ml4 +++ b/contrib/setoid_ring/newring.ml4 @@ -217,15 +217,19 @@ let coq_Some = coq_constant "Some" let lapp f args = mkApp(Lazy.force f,args) +let dest_rel0 t = + match kind_of_term t with + | App(f,args) when Array.length args >= 2 -> + let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in + if closed0 rel then + (rel,args.(Array.length args - 2),args.(Array.length args - 1)) + else error "ring: cannot find relation (not closed)" + | _ -> error "ring: cannot find relation" + let rec dest_rel t = match kind_of_term t with - App(f,args) when Array.length args >= 2 -> - let rel = mkApp(f,Array.sub args 0 (Array.length args - 2)) in - if closed0 rel then - (rel,args.(Array.length args - 2),args.(Array.length args - 1)) - else error "ring: cannot find relation (not closed)" - | Prod(_,_,c) -> dest_rel c - | _ -> error "ring: cannot find relation" + | Prod(_,_,c) -> dest_rel c + | _ -> dest_rel0 t (****************************************************************************) (* Library linking *) @@ -299,9 +303,9 @@ let _ = add_map "ring" coq_nil, (function -1->Eval|_ -> Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot); + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot)]) @@ -335,7 +339,7 @@ let ring_lookup_by_name ref = Spmap.find (Nametab.locate_obj (snd(qualid_of_reference ref))) !from_name -let find_ring_structure env sigma l cl oname = +let find_ring_structure env sigma l oname = match oname, l with Some rf, _ -> (try ring_lookup_by_name rf @@ -356,13 +360,14 @@ let find_ring_structure env sigma l cl oname = errorlabstrm "ring" (str"cannot find a declared ring structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> + | None, [] -> assert false +(* let (req,_,_) = dest_rel cl in (try ring_for_relation req with Not_found -> errorlabstrm "ring" (str"cannot find a declared ring structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) + spc()++str"\""++pr_constr req++str"\"")) *) let _ = Summary.declare_summary "tactic-new-ring-table" @@ -688,21 +693,23 @@ END (* The tactics consist then only in a lookup in the ring database and call the appropriate ltac. *) -let make_term_list carrier rl gl = - let rl = - match rl with - [] -> let (_,t1,t2) = dest_rel (pf_concl gl) in [t1;t2] - | _ -> rl in +let make_args_list rl t = + match rl with + | [] -> let (_,t1,t2) = dest_rel0 t in [t1;t2] + | _ -> rl + +let make_term_list carrier rl = List.fold_right (fun x l -> lapp coq_cons [|carrier;x;l|]) rl (lapp coq_nil [|carrier|]) -let ring_lookup (f:glob_tactic_expr) lH rl gl = +let ring_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in - let e = find_ring_structure env sigma rl (pf_concl gl) None in - let rl = carg (make_term_list e.ring_carrier rl gl) in + let rl = make_args_list rl t in + let e = find_ring_structure env sigma rl None in + let rl = carg (make_term_list e.ring_carrier rl) in let lH = carg (make_hyp_list env lH) in let req = carg e.ring_req in let sth = carg e.ring_setoid in @@ -723,8 +730,9 @@ let ring_lookup (f:glob_tactic_expr) lH rl gl = lemma1;lemma2;pretac;posttac;lH;rl])) gl TACTIC EXTEND ring_lookup -| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr)] -> - [ring_lookup (fst f) lH lr] +| [ "ring_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(lr) + "[" constr(t) "]" ] -> + [ring_lookup (fst f) lH lr t] END @@ -745,14 +753,14 @@ let _ = add_map "field" (* display_linear: evaluate polynomials and coef operations, protect field operations and make recursive call on the var map *) my_constant "display_linear", - (function -1|8|9|10|11|12|13|14|16|17->Eval|15->Rec|_->Prot); + (function -1|9|10|11|12|13|15|16->Eval|14->Rec|_->Prot); my_constant "display_pow_linear", - (function -1|8|9|10|11|12|13|14|15|17|19|20->Eval|18->Rec|_->Prot); + (function -1|9|10|11|12|13|14|16|18|19->Eval|17->Rec|_->Prot); (* Pphi_dev: evaluate polynomial and coef operations, protect ring operations and make recursive call on the var map *) - pol_cst "Pphi_dev", (function -1|8|9|10|11|12|13|15->Eval|14->Rec|_->Prot); + pol_cst "Pphi_dev", (function -1|8|9|10|11|12|14->Eval|13->Rec|_->Prot); pol_cst "Pphi_pow", - (function -1|8|9|10|11|12|14|16|18->Eval|17->Rec|_->Prot); + (function -1|8|9|10|11|13|15|17->Eval|16->Rec|_->Prot); (* PEeval: evaluate morphism and polynomial, protect ring operations and make recursive call on the var map *) pol_cst "PEeval", (function -1|7|9|12->Eval|11->Rec|_->Prot); @@ -805,6 +813,7 @@ type field_info = field_ok : constr; field_simpl_eq_ok : constr; field_simpl_ok : constr; + field_simpl_eq_in_ok : constr; field_cond : constr; field_pre_tac : glob_tactic_expr; field_post_tac : glob_tactic_expr } @@ -821,7 +830,7 @@ let field_lookup_by_name ref = !field_from_name -let find_field_structure env sigma l cl oname = +let find_field_structure env sigma l oname = check_required_library (cdir@["Field_tac"]); match oname, l with Some rf, _ -> @@ -843,13 +852,13 @@ let find_field_structure env sigma l cl oname = errorlabstrm "field" (str"cannot find a declared field structure over"++ spc()++str"\""++pr_constr ty++str"\"")) - | None, [] -> - let (req,_,_) = dest_rel cl in + | None, [] -> assert false +(* let (req,_,_) = dest_rel cl in (try field_for_relation req with Not_found -> errorlabstrm "field" (str"cannot find a declared field structure for equality"++ - spc()++str"\""++pr_constr req++str"\"")) + spc()++str"\""++pr_constr req++str"\"")) *) let _ = Summary.declare_summary "tactic-new-field-table" @@ -883,7 +892,8 @@ let subst_th (_,subst,th) = let thm1' = subst_mps subst th.field_ok in let thm2' = subst_mps subst th.field_simpl_eq_ok in let thm3' = subst_mps subst th.field_simpl_ok in - let thm4' = subst_mps subst th.field_cond in + let thm4' = subst_mps subst th.field_simpl_eq_in_ok in + let thm5' = subst_mps subst th.field_cond in let tac'= subst_tactic subst th.field_cst_tac in let pow_tac' = subst_tactic subst th.field_pow_tac in let pretac'= subst_tactic subst th.field_pre_tac in @@ -893,7 +903,8 @@ let subst_th (_,subst,th) = thm1' == th.field_ok && thm2' == th.field_simpl_eq_ok && thm3' == th.field_simpl_ok && - thm4' == th.field_cond && + thm4' == th.field_simpl_eq_in_ok && + thm5' == th.field_cond && tac' == th.field_cst_tac && pow_tac' == th.field_pow_tac && pretac' == th.field_pre_tac && @@ -906,7 +917,8 @@ let subst_th (_,subst,th) = field_ok = thm1'; field_simpl_eq_ok = thm2'; field_simpl_ok = thm3'; - field_cond = thm4'; + field_simpl_eq_in_ok = thm4'; + field_cond = thm5'; field_pre_tac = pretac'; field_post_tac = posttac' } @@ -953,19 +965,21 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = let inv_m = default_field_equality r inv req in let rk = reflect_coeff morphth in let params = - exec_tactic env 8 (field_ltac"field_lemmas") + exec_tactic env 9 (field_ltac"field_lemmas") (List.map carg[sth;ext;inv_m;fth;pspec;sspec;rk]) in let lemma1 = constr_of params.(3) in let lemma2 = constr_of params.(4) in let lemma3 = constr_of params.(5) in + let lemma4 = constr_of params.(6) in let cond_lemma = match inj with - | Some thm -> mkApp(constr_of params.(7),[|thm|]) - | None -> constr_of params.(6) in + | Some thm -> mkApp(constr_of params.(8),[|thm|]) + | None -> constr_of params.(7) in let lemma1 = decl_constant (string_of_id name^"_field_lemma1") lemma1 in let lemma2 = decl_constant (string_of_id name^"_field_lemma2") lemma2 in let lemma3 = decl_constant (string_of_id name^"_field_lemma3") lemma3 in - let cond_lemma = decl_constant (string_of_id name^"_lemma4") cond_lemma in + let lemma4 = decl_constant (string_of_id name^"_field_lemma4") lemma4 in + let cond_lemma = decl_constant (string_of_id name^"_lemma5") cond_lemma in let cst_tac = interp_cst_tac kind (zero,one,add,mul,opp) cst_tac in let pretac = match pre with @@ -985,6 +999,7 @@ let add_field_theory name fth eqth morphth cst_tac inj (pre,post) power sign = field_ok = lemma1; field_simpl_eq_ok = lemma2; field_simpl_ok = lemma3; + field_simpl_eq_in_ok = lemma4; field_cond = cond_lemma; field_pre_tac = pretac; field_post_tac = posttac }) in () @@ -1026,11 +1041,12 @@ VERNAC COMMAND EXTEND AddSetoidField add_field_theory id (ic t) set k cst_tac inj (pre,post) power sign] END -let field_lookup (f:glob_tactic_expr) lH rl gl = +let field_lookup (f:glob_tactic_expr) lH rl t gl = let env = pf_env gl in let sigma = project gl in - let e = find_field_structure env sigma rl (pf_concl gl) None in - let rl = carg (make_term_list e.field_carrier rl gl) in + let rl = make_args_list rl t in + let e = find_field_structure env sigma rl None in + let rl = carg (make_term_list e.field_carrier rl) in let lH = carg (make_hyp_list env lH) in let req = carg e.field_req in let cst_tac = Tacexp e.field_cst_tac in @@ -1038,6 +1054,7 @@ let field_lookup (f:glob_tactic_expr) lH rl gl = let field_ok = carg e.field_ok in let field_simpl_ok = carg e.field_simpl_ok in let field_simpl_eq_ok = carg e.field_simpl_eq_ok in + let field_simpl_eq_in_ok = carg e.field_simpl_eq_in_ok in let cond_ok = carg e.field_cond in let pretac = Tacexp(TacFun([None],e.field_pre_tac)) in let posttac = Tacexp(TacFun([None],e.field_post_tac)) in @@ -1045,10 +1062,11 @@ let field_lookup (f:glob_tactic_expr) lH rl gl = (TacLetIn ([(dummy_loc,id_of_string"f"),None,Tacexp f], ltac_lcall "f" - [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok;cond_ok; - pretac;posttac;lH;rl])) gl + [req;cst_tac;pow_tac;field_ok;field_simpl_ok;field_simpl_eq_ok; + field_simpl_eq_in_ok;cond_ok;pretac;posttac;lH;rl])) gl TACTIC EXTEND field_lookup -| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) ] -> - [ field_lookup (fst f) lH l ] +| [ "field_lookup" tactic(f) "[" constr_list(lH) "]" constr_list(l) + "[" constr(t) "]" ] -> + [ field_lookup (fst f) lH l t ] END -- cgit v1.2.3