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)
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)
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 *)
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 <uri, typeno, consno> 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 <uri, typeno> 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 *)
(**
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
@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.
/ \
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 *)
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
abstraction function:
concrete polynoms -----> (abstract polynoms, varmap)
@param terms list of conrete polynoms
- @param proof current proof
@return a pair <aterms, varmap> 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 *)
(* "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;
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)
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
-
-(** AUX TACTIC{,AL}S *)
+ (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
- (**
- naive implementation of ORELSE tactical, try a sequence of tactics in turn:
- if one fails pass to the next one and so on, eventually raises (failure "no
- tactics left")
- TODO warning: not tail recursive due to "try .. with" boxing
- *)
-let rec try_tactics ~(tactics: (string * tactic) list) ~status =
- warn "in Ring.try_tactics";
- match tactics with
- | (descr, tac)::tactics ->
- warn ("Ring.try_tactics IS TRYING " ^ descr);
- (try
- let res = tac ~status in
- warn ("Ring.try_tactics: " ^ descr ^ " succedeed!!!");
- res
- with
- e ->
- match e with
- (Fail _)
- | (CicTypeChecker.NotWellTyped _)
- | (CicUnification.UnificationFailed) ->
- warn (
- "Ring.try_tactics failed with exn: " ^
- Printexc.to_string e);
- try_tactics ~tactics ~status
- | _ -> raise e (* [e] must not be caught ; let's re-raise it *)
- )
- | [] -> raise (Fail "try_tactics: no tactics left")
-
-let thens ~start ~continuations ~status =
- let (proof,new_goals) = start ~status in
- try
- List.fold_left2
- (fun (proof,goals) goal tactic ->
- let (proof',new_goals') = tactic ~status:(proof,goal) in
- (proof',goals@new_goals')
- ) (proof,[]) new_goals continuations
- with
- Invalid_argument _ -> raise (Fail "thens: wrong number of new goals")
-
-let id_tac ~status:(proof,goal) =
- (proof,[goal])
let status_of_single_goal_tactic_result =
function
*)
let elim_type_tac ~term ~status =
warn "in Ring.elim_type_tac";
- thens ~start:(cut_tac ~term)
- ~continuations:[elim_intros_simpl_tac ~term:(Cic.Rel 1) ; id_tac] ~status
+ Tacticals.thens ~start:(cut_tac ~term)
+ ~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
*)
let elim_type2_tac ~term ~proof ~status =
warn "in Ring.elim_type2";
- thens ~start:(elim_type_tac ~term)
- ~continuations:[id_tac ; exact_tac ~term:proof] ~status
+ Tacticals.thens ~start:(elim_type_tac ~term)
+ ~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
*)
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) =
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) ->
t2; t2'; t2''; t2'_eq_t2'']);
try
let new_hyps = ref 0 in (* number of new hypotheses created *)
- try_tactics
+ 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
lift 1 (t1,t1',t1'',t1'_eq_t1'', t2,t2',t2'',t2'_eq_t2'')
in
let status'' =
- try_tactics (* try to solve 1st subgoal *)
+ Tacticals.try_tactics (* try to solve 1st subgoal *)
~status:status'
~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
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')]
projects / helm.git / blobdiff