X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2Fring.ml;h=399d2c2892334297ed970f25b47fe363ede544e8;hb=347d3c4262af67b378f4a65f735f48797ffc37a3;hp=953ed64445d7bbbf7d9cf7a2f3d4efd464ddcb7a;hpb=71922d0022ee8f9e507f601dc93a2f68c2080d85;p=helm.git diff --git a/helm/gTopLevel/ring.ml b/helm/gTopLevel/ring.ml index 953ed6444..399d2c289 100644 --- a/helm/gTopLevel/ring.ml +++ b/helm/gTopLevel/ring.ml @@ -48,8 +48,13 @@ let warn s = let eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind" let refl_eqt_uri = (eqt_uri, 0, 1) -let sym_eqt_uri = - uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/sym_eqT.con" +let equality_is_a_congruence_A = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/A.var" +let equality_is_a_congruence_x = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/x.var" +let equality_is_a_congruence_y = + uri_of_string "cic:/Coq/Init/Logic_Type/Equality_is_a_congruence/y.var" +let sym_eqt_uri = uri_of_string "cic:/Coq/Init/Logic_Type/sym_eqT.con" let bool_uri = uri_of_string "cic:/Coq/Init/Datatypes/bool.ind" let true_uri = (bool_uri, 0, 1) let false_uri = (bool_uri, 0, 2) @@ -63,8 +68,7 @@ let r1_uri = uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" let rtheory_uri = uri_of_string "cic:/Coq/Reals/Rbase/RTheory.con" let apolynomial_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial.ind" + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial.ind" let apvar_uri = (apolynomial_uri, 0, 1) let ap0_uri = (apolynomial_uri, 0, 2) let ap1_uri = (apolynomial_uri, 0, 3) @@ -72,28 +76,41 @@ let applus_uri = (apolynomial_uri, 0, 4) let apmult_uri = (apolynomial_uri, 0, 5) let apopp_uri = (apolynomial_uri, 0, 6) -let varmap_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap.ind" +let quote_varmap_A_uri = uri_of_string "cic:/Coq/ring/Quote/variables_map/A.var" +let varmap_uri = uri_of_string "cic:/Coq/ring/Quote/varmap.ind" let empty_vm_uri = (varmap_uri, 0, 1) let node_vm_uri = (varmap_uri, 0, 2) -let varmap_find_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/varmap_find.con" -let index_uri = - uri_of_string "cic:/Coq/ring/Quote/variables_map/index.ind" +let varmap_find_uri = uri_of_string "cic:/Coq/ring/Quote/varmap_find.con" +let index_uri = uri_of_string "cic:/Coq/ring/Quote/index.ind" let left_idx_uri = (index_uri, 0, 1) let right_idx_uri = (index_uri, 0, 2) let end_idx_uri = (index_uri, 0, 3) -let interp_ap_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_ap.con" +let abstract_rings_A_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/A.var" +let abstract_rings_Aplus_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aplus.var" +let abstract_rings_Amult_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Amult.var" +let abstract_rings_Aone_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aone.var" +let abstract_rings_Azero_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Azero.var" +let abstract_rings_Aopp_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aopp.var" +let abstract_rings_Aeq_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/Aeq.var" +let abstract_rings_vm_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/vm.var" +let abstract_rings_T_uri = + uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/T.var" +let interp_ap_uri = uri_of_string "cic:/Coq/ring/Ring_abstract/interp_ap.con" let interp_sacs_uri = - uri_of_string "cic:/Coq/ring/Ring_abstract/abstract_rings/interp_sacs.con" + uri_of_string "cic:/Coq/ring/Ring_abstract/interp_sacs.con" let apolynomial_normalize_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize.con" + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize.con" let apolynomial_normalize_ok_uri = - uri_of_string - "cic:/Coq/ring/Ring_abstract/abstract_rings/apolynomial_normalize_ok.con" + uri_of_string "cic:/Coq/ring/Ring_abstract/apolynomial_normalize_ok.con" (** CIC PREDICATES *) @@ -157,30 +174,29 @@ let context_of_status ~status:(proof, goal as status) = Create a Cic term consisting of a constant @param uri URI of the constant @proof current proof + @exp_named_subst explicit named substitution *) -let mkConst ~uri ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.Const (uri, cookingsno) +let mkConst ~uri ~exp_named_subst = + Cic.Const (uri, exp_named_subst) (** Create a Cic term consisting of a constructor @param uri triple where uri is the uri of an inductive type, typeno is the type number in a mutind structure (0 based), consno is the constructor number (1 based) - @param proof current proof + @exp_named_subst explicit named substitution *) -let mkCtor ~uri:(uri, typeno, consno) ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.MutConstruct (uri, cookingsno, typeno, consno) +let mkCtor ~uri:(uri, typeno, consno) ~exp_named_subst = + Cic.MutConstruct (uri, typeno, consno, exp_named_subst) (** Create a Cic term consisting of a type member of a mutual induction @param uri pair where uri is the uri of a mutual inductive type and typeno is the type number (0 based) in the mutual induction + @exp_named_subst explicit named substitution *) -let mkMutInd ~uri:(uri, typeno) ~proof = - let cookingsno = relative_depth (uri_of_proof ~proof) uri 0 in - Cic.MutInd (uri, cookingsno, typeno) +let mkMutInd ~uri:(uri, typeno) ~exp_named_subst = + Cic.MutInd (uri, typeno, exp_named_subst) (** EXCEPTIONS *) @@ -195,12 +211,12 @@ exception GoalUnringable (** Check whether the ring tactic can be applied on a given term (i.e. that is an equality on reals) - @param term term to be tested + @param term to be tested @return true if the term is ringable, false otherwise *) let ringable = let is_equality = function - | Cic.MutInd uri _ 0 when (eq uri eqt_uri) -> true + | Cic.MutInd uri 0 [] when (eq uri eqt_uri) -> true | _ -> false in let is_real = function @@ -238,17 +254,17 @@ let split_eq = function @return an index representing the same node in a varmap (@see varmap_uri), the returned index is as defined in index (@see index_uri) *) -let path_of_int n proof = +let path_of_int n = let rec digits_of_int n = if n=1 then [] else (n mod 2 = 1)::(digits_of_int (n lsr 1)) in List.fold_right (fun digit path -> Cic.Appl [ - mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) proof; + mkCtor (if (digit = true) then right_idx_uri else left_idx_uri) []; path]) (List.rev (digits_of_int n)) (* remove leading true (i.e. digit 1) *) - (mkCtor end_idx_uri proof) + (mkCtor end_idx_uri []) (** Build a variable map (@see varmap_uri) from a variables array. @@ -259,15 +275,12 @@ let path_of_int n proof = / \ y z @param vars variables array - @param proof current proof @return a cic term representing the variable map containing vars variables *) -let btree_of_array ~vars ~proof = - let r = mkConst r_uri proof in (* cic objects *) - let empty_vm = mkCtor empty_vm_uri proof in - let empty_vm_r = Cic.Appl [empty_vm; r] in - let node_vm = mkCtor node_vm_uri proof in - let node_vm_r = Cic.Appl [node_vm; r] in +let btree_of_array ~vars = + let r = mkConst r_uri [] in (* cic objects *) + let empty_vm_r = mkCtor empty_vm_uri [quote_varmap_A_uri,r] in + let node_vm_r = mkCtor node_vm_uri [quote_varmap_A_uri,r] in let size = Array.length vars in let halfsize = size lsr 1 in let rec aux n = (* build the btree starting from position n *) @@ -278,9 +291,9 @@ let btree_of_array ~vars ~proof = if n > size then empty_vm_r else if n > halfsize then (* no more children *) - Cic.Appl [node_vm; r; vars.(n-1); empty_vm_r; empty_vm_r] + Cic.Appl [node_vm_r; vars.(n-1); empty_vm_r; empty_vm_r] else (* still children *) - Cic.Appl [node_vm; r; vars.(n-1); aux (n*2); aux (n*2+1)] + Cic.Appl [node_vm_r; vars.(n-1); aux (n*2); aux (n*2+1)] in aux 1 @@ -288,11 +301,10 @@ let btree_of_array ~vars ~proof = abstraction function: concrete polynoms -----> (abstract polynoms, varmap) @param terms list of conrete polynoms - @param proof current proof @return a pair where aterms is a list of abstract polynoms and varmap is the variable map needed to interpret them *) -let abstract_poly ~terms ~proof = +let abstract_poly ~terms = let varhash = Hashtbl.create 19 in (* vars hash, to speed up lookup *) let varlist = ref [] in (* vars list in reverse order *) let counter = ref 1 in (* index of next new variable *) @@ -300,23 +312,23 @@ let abstract_poly ~terms ~proof = (* "bop" -> binary operator | "uop" -> unary operator *) | Cic.Appl (bop::t1::t2::[]) when (cic_is_const ~uri:(Some rplus_uri) bop) -> (* +. *) - Cic.Appl [mkCtor applus_uri proof; aux t1; aux t2] + Cic.Appl [mkCtor applus_uri []; aux t1; aux t2] | Cic.Appl (bop::t1::t2::[]) when (cic_is_const ~uri:(Some rmult_uri) bop) -> (* *. *) - Cic.Appl [mkCtor apmult_uri proof; aux t1; aux t2] + Cic.Appl [mkCtor apmult_uri []; aux t1; aux t2] | Cic.Appl (uop::t::[]) when (cic_is_const ~uri:(Some ropp_uri) uop) -> (* ~-. *) - Cic.Appl [mkCtor apopp_uri proof; aux t] + Cic.Appl [mkCtor apopp_uri []; aux t] | t when (cic_is_const ~uri:(Some r0_uri) t) -> (* 0. *) - mkCtor ap0_uri proof + mkCtor ap0_uri [] | t when (cic_is_const ~uri:(Some r1_uri) t) -> (* 1. *) - mkCtor ap1_uri proof + mkCtor ap1_uri [] | t -> (* variable *) try Hashtbl.find varhash t (* use an old var *) with Not_found -> begin (* create a new var *) let newvar = - Cic.Appl [mkCtor apvar_uri proof; path_of_int !counter proof] + Cic.Appl [mkCtor apvar_uri []; path_of_int !counter] in incr counter; varlist := t :: !varlist; @@ -326,7 +338,7 @@ let abstract_poly ~terms ~proof = in let aterms = List.map aux terms in (* abstract vars *) let varmap = (* build varmap *) - btree_of_array ~vars:(Array.of_list (List.rev !varlist)) ~proof + btree_of_array ~vars:(Array.of_list (List.rev !varlist)) in (aterms, varmap) @@ -338,39 +350,53 @@ let abstract_poly ~terms ~proof = t''' = apolynomial_normalize_ok(varmap, at) at is the abstract term built from t, t is a single member of aterms *) -let build_segments ~terms ~proof = - let r = mkConst r_uri proof in (* cic objects *) - let rplus = mkConst rplus_uri proof in - let rmult = mkConst rmult_uri proof in - let ropp = mkConst ropp_uri proof in - let r0 = mkConst r0_uri proof in - let r1 = mkConst r1_uri proof in - let interp_ap = mkConst interp_ap_uri proof in - let interp_sacs = mkConst interp_sacs_uri proof in - let apolynomial_normalize = mkConst apolynomial_normalize_uri proof in - let apolynomial_normalize_ok = mkConst apolynomial_normalize_ok_uri proof in - let rtheory = mkConst rtheory_uri proof in +let build_segments ~terms = + let r = mkConst r_uri [] in (* cic objects *) + let rplus = mkConst rplus_uri [] in + let rmult = mkConst rmult_uri [] in + let ropp = mkConst ropp_uri [] in + let r1 = mkConst r1_uri [] in + let r0 = mkConst r0_uri [] in + let theory_args_subst varmap = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_vm_uri, varmap] in + let theory_args_subst' eq varmap t = + [abstract_rings_A_uri, r ; + abstract_rings_Aplus_uri, rplus ; + abstract_rings_Amult_uri, rmult ; + abstract_rings_Aone_uri, r1 ; + abstract_rings_Azero_uri, r0 ; + abstract_rings_Aopp_uri, ropp ; + abstract_rings_Aeq_uri, eq ; + abstract_rings_vm_uri, varmap ; + abstract_rings_T_uri, t] in + let interp_ap varmap = + mkConst interp_ap_uri (theory_args_subst varmap) in + let interp_sacs varmap = + mkConst interp_sacs_uri (theory_args_subst varmap) in + let apolynomial_normalize = mkConst apolynomial_normalize_uri [] in + let apolynomial_normalize_ok eq varmap t = + mkConst apolynomial_normalize_ok_uri (theory_args_subst' eq varmap t) in + let rtheory = mkConst rtheory_uri [] in let lxy_false = (** Cic funcion "fun (x,y):R -> false" *) - Cic.Lambda (Cic.Anonimous, r, - Cic.Lambda (Cic.Anonimous, r, - mkCtor false_uri proof)) + Cic.Lambda (Cic.Anonymous, r, + Cic.Lambda (Cic.Anonymous, r, + mkCtor false_uri [])) in - let theory_args = [r; rplus; rmult; r1; r0; ropp] in - let (aterms, varmap) = abstract_poly ~terms ~proof in (* abstract polys *) + let (aterms, varmap) = abstract_poly ~terms in (* abstract polys *) List.map (* build ring segments *) - (fun t -> - Cic.Appl ((interp_ap :: theory_args) @ [varmap; t]), - Cic.Appl ( - interp_sacs :: - (theory_args @ - [varmap; Cic.Appl [apolynomial_normalize; t]])), - Cic.Appl ( - (apolynomial_normalize_ok :: theory_args) @ - [lxy_false; varmap; rtheory; t])) - aterms - -let id_tac ~status:(proof,goal) = - (proof,[goal]) + (fun t -> + Cic.Appl [interp_ap varmap ; t], + Cic.Appl ( + [interp_sacs varmap ; Cic.Appl [apolynomial_normalize; t]]), + Cic.Appl [apolynomial_normalize_ok lxy_false varmap rtheory ; t] + ) aterms + let status_of_single_goal_tactic_result = function @@ -386,7 +412,7 @@ let status_of_single_goal_tactic_result = let elim_type_tac ~term ~status = warn "in Ring.elim_type_tac"; Tacticals.thens ~start:(cut_tac ~term) - ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status + ~continuations:[elim_simpl_intros_tac ~term:(Cic.Rel 1) ; Tacticals.id_tac] ~status (** auxiliary tactic, use elim_type and try to close 2nd subgoal using proof @@ -397,8 +423,9 @@ let elim_type_tac ~term ~status = let elim_type2_tac ~term ~proof ~status = warn "in Ring.elim_type2"; Tacticals.thens ~start:(elim_type_tac ~term) - ~continuations:[id_tac ; exact_tac ~term:proof] ~status + ~continuations:[Tacticals.id_tac ; exact_tac ~term:proof] ~status +(* spostata in variousTactics.ml (** Reflexivity tactic, try to solve current goal using "refl_eqT" Warning: this isn't equale to the coq's Reflexivity because this one tries @@ -407,12 +434,13 @@ let elim_type2_tac ~term ~proof ~status = *) let reflexivity_tac ~status:(proof, goal) = warn "in Ring.reflexivity_tac"; - let refl_eqt = mkCtor ~uri:refl_eqt_uri ~proof:proof in + let refl_eqt = mkCtor ~uri:refl_eqt_uri ~exp_named_subst:[] in try apply_tac ~status:(proof, goal) ~term:refl_eqt with (Fail _) as e -> let e_str = Printexc.to_string e in raise (Fail ("Reflexivity failed with exception: " ^ e_str)) +*) (** lift an 8-uple of debrujins indexes of n *) let lift ~n (a,b,c,d,e,f,g,h) = @@ -448,15 +476,14 @@ let purge_hyps_tac ~count ~status:(proof, goal as status) = Ring tactic, does associative and commutative rewritings in Reals ring @param status current proof engine status *) -let ring_tac ~status:(proof, goal) = +let ring_tac ~status:((proof, goal) as status) = warn "in Ring tactic"; - let status = (proof, goal) in - let eqt = mkMutInd (eqt_uri, 0) proof in - let r = mkConst r_uri proof in + let eqt = mkMutInd (eqt_uri, 0) [] in + let r = mkConst r_uri [] in let metasenv = metasenv_of_status ~status in let (metano, context, ty) = conj_of_metano goal metasenv in let (t1, t2) = split_eq ty in (* goal like t1 = t2 *) - match (build_segments ~terms:[t1; t2] ~proof) with + match (build_segments ~terms:[t1; t2]) with | (t1', t1'', t1'_eq_t1'')::(t2', t2'', t2'_eq_t2'')::[] -> begin List.iter (* debugging, feel free to remove *) (fun (descr, term) -> @@ -471,13 +498,19 @@ let ring_tac ~status:(proof, goal) = Tacticals.try_tactics ~status ~tactics:[ - "reflexivity", reflexivity_tac; - "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1''; - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; - "exact sym_eqt su t1 ...", exact_tac ~term:( - Cic.Appl [ - mkConst sym_eqt_uri proof; mkConst r_uri proof; - t1''; t1; t1'_eq_t1'']); + "reflexivity", VariousTactics.reflexivity_tac ; + "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; + "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; + "exact sym_eqt su t1 ...", exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t1'' ; + equality_is_a_congruence_y, t1 + ] ; + t1'_eq_t1'' + ]) ; "elim_type eqt su t1 ...", (fun ~status -> let status' = (* status after 1st elim_type use *) let context = context_of_status ~status in @@ -506,11 +539,16 @@ let ring_tac ~status:(proof, goal) = ~tactics:[ "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; "exact sym_eqt su t2 ...", - exact_tac ~term:( - Cic.Appl [ - mkConst sym_eqt_uri proof; - mkConst r_uri proof; - t2''; t2; t2'_eq_t2'']); + exact_tac + ~term:( + Cic.Appl + [mkConst sym_eqt_uri + [equality_is_a_congruence_A, mkConst r_uri [] ; + equality_is_a_congruence_x, t2'' ; + equality_is_a_congruence_y, t2 + ] ; + t2'_eq_t2'' + ]) ; "elim_type eqt su t2 ...", (fun ~status -> let status' = let context = context_of_status ~status in @@ -532,7 +570,7 @@ let ring_tac ~status:(proof, goal) = in try (* try to solve main goal *) warn "trying reflexivity ...."; - reflexivity_tac ~status:status' + VariousTactics.reflexivity_tac ~status:status' with (Fail _) -> (* leave conclusion to the user *) warn "reflexivity failed, solution's left as an ex :-)"; purge_hyps_tac ~count:!new_hyps ~status:status')]