(**** TABLES ****)
-let default_eq_URIs =
- [HelmLibraryObjects.Logic.eq_URI,
- HelmLibraryObjects.Logic.sym_eq_URI,
- HelmLibraryObjects.Logic.trans_eq_URI,
- HelmLibraryObjects.Logic.eq_ind_URI,
- HelmLibraryObjects.Logic.eq_ind_r_URI];;
-
-let default_true_URIs = [HelmLibraryObjects.Logic.true_URI]
-let default_false_URIs = [HelmLibraryObjects.Logic.false_URI]
-let default_absurd_URIs = [HelmLibraryObjects.Logic.absurd_URI]
+let default_eq_URIs = []
+let default_true_URIs = []
+let default_false_URIs = []
+let default_absurd_URIs = []
(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
-let eq_URIs_ref =
- ref [HelmLibraryObjects.Logic.eq_URI,
- HelmLibraryObjects.Logic.sym_eq_URI,
- HelmLibraryObjects.Logic.trans_eq_URI,
- HelmLibraryObjects.Logic.eq_ind_URI,
- HelmLibraryObjects.Logic.eq_ind_r_URI];;
+let eq_URIs_ref = ref default_eq_URIs;;
-let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI]
-let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI]
-let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
+let true_URIs_ref = ref default_true_URIs
+let false_URIs_ref = ref default_false_URIs
+let absurd_URIs_ref = ref default_absurd_URIs
(**** SET_DEFAULT ****)
(**** LOOKUP FUNCTIONS ****)
-let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq
+let eq_URI () =
+ try let eq,_,_,_,_ = List.hd !eq_URIs_ref in Some eq
+ with Failure "hd" -> None
let is_eq_URI uri =
List.exists (fun (eq,_,_,_,_) -> UriManager.eq eq uri) !eq_URIs_ref
let _,_,_,_,x = List.find (fun eq,_,_,_,_ -> UriManager.eq eq uri) !eq_URIs_ref in x
with Not_found -> raise (NotRecognized (UriManager.string_of_uri uri))
-let true_URI () = List.hd !true_URIs_ref
-let false_URI () = List.hd !false_URIs_ref
-let absurd_URI () = List.hd !absurd_URIs_ref
+let true_URI () =
+ try Some (List.hd !true_URIs_ref) with Failure "hd" -> None
+let false_URI () =
+ try Some (List.hd !false_URIs_ref) with Failure "hd" -> None
+let absurd_URI () =
+ try Some (List.hd !absurd_URIs_ref) with Failure "hd" -> None
val set_default : string -> UriManager.uri list -> unit
val reset_defaults : unit -> unit
-val eq_URI : unit -> UriManager.uri
+val eq_URI : unit -> UriManager.uri option
val is_eq_URI : UriManager.uri -> bool
val is_eq_ind_URI : UriManager.uri -> bool
val sym_eq_URI : eq:UriManager.uri -> UriManager.uri
-val false_URI : unit -> UriManager.uri
-val true_URI : unit -> UriManager.uri
-val absurd_URI : unit -> UriManager.uri
+val false_URI : unit -> UriManager.uri option
+val true_URI : unit -> UriManager.uri option
+val absurd_URI : unit -> UriManager.uri option
| Cic.InductiveDefinition (_,_,_,attrs) ->
uris := !uris @
generate_elimination_principles uri refinement_toolkit;
- (* uris := !uris @ generate_inversion refinement_toolkit uri obj; *)
+ uris := !uris @ generate_inversion refinement_toolkit uri obj;
let rec get_record_attrs =
function
| [] -> None
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
+ let true_URI =
+ match LibraryObjects.true_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
+ let false_URI =
+ match LibraryObjects.false_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in
let fail msg = raise (ProofEngineTypes.Fail (lazy ("Discriminate: " ^ msg))) in
let find_discriminating_consno t1 t2 =
let rec aux t1 t2 =
C.Lambda (binder, source, (aux target (k+1)))
| _ ->
if (id = false_constr_id)
- then (C.MutInd(LibraryObjects.false_URI (),0,[]))
- else (C.MutInd(LibraryObjects.true_URI (),0,[]))
+ then (C.MutInd(false_URI,0,[]))
+ else (C.MutInd(true_URI,0,[]))
in
(CicSubstitution.lift 1 (aux red_ty 1)))
constructor_list
let (proof',goals') =
ProofEngineTypes.apply_tactic
(EliminationTactics.elim_type_tac
- (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+ (C.MutInd (false_URI, 0, [])))
status
in
(match goals' with
let uri,metasenv,pbo,pty = proof in
let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
assert (hyps_pat = []); (*CSC: not implemented yet *)
+ let eq_URI =
+ match LibraryObjects.eq_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command"))
+ in
let context_len = List.length context in
let subst,metasenv,u,_,selected_terms_with_context =
ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
~start:(
P.cut_tac
(C.Appl [
- (C.MutInd (LibraryObjects.eq_URI (), 0, [])) ;
+ (C.MutInd (eq_URI, 0, [])) ;
ty_of_with_what ;
what ;
with_what]))
(get_sort_type paramty)
(Cic.Sort Cic.Prop)) != 0)
+exception EqualityNotDefinedYet
let private_inversion_tac ~term =
let module T = CicTypeChecker in
let module R = CicReduction in
(*DEBUG*) debug_print (lazy ("private inversion begins"));
let (_,metasenv,_,_) = proof in
- let uri_of_eq = LibraryObjects.eq_URI () in
+ let uri_of_eq =
+ match LibraryObjects.eq_URI () with
+ None -> raise EqualityNotDefinedYet
+ | Some uri -> uri
+ in
let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let uri = baseuri_of_term termty in
*)
val isSetType: Cic.term -> bool
+exception EqualityNotDefinedYet (* raised by private_inversion_tac only *)
val private_inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
val inversion_tac: term: Cic.term -> ProofEngineTypes.tactic
if List.length (list_of_prod arity) = (nleft + 1) then
None
else
- begin
+ try
let arity_l = cut_last (list_of_prod arity) in
let rightparam_tys = cut_first nleft arity_l in
let theorem = build_theorem rightparam_tys arity_l arity cons_list
Some
(inversor_uri,
Cic.Constant (UriManager.name_of_uri inversor_uri,Some bo,ty,[],[]))
- end
+ with
+ Inversion.EqualityNotDefinedYet -> None
;;
let init () = ();;
(* match main with *)
(* None -> raise Goal_is_not_an_equation *)
(* | Some (m,l) -> *)
- let m, l =
+ let l =
let eq_URI =
- let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
- UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+ match LibraryObjects.eq_URI () with
+ None -> None
+ | Some s ->
+ Some
+ (UriManager.uri_of_string
+ (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
in
- match main with
- | None -> eq_URI, []
- | Some (m, l) when UriManager.eq m eq_URI -> m, l
- | Some (m, l) -> eq_URI, []
+ match eq_URI,main with
+ | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
+ | _,_ -> []
in
Printf.printf "\nSome (m, l): %s, [%s]\n\n"
- (UriManager.string_of_uri m)
- (String.concat "; " (List.map UriManager.string_of_uri l));
+ (UriManager.string_of_uri (List.hd l))
+ (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
(* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
let set = signature_of_hypothesis context in
(* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
(* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
let set = close_with_constructors set metasenv context in
(* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
- let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let set = List.fold_right Constr.UriManagerSet.remove l set in
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
let uris = List.filter nonvar (List.map snd uris) in
let module P = PrimitiveTactics in
let _,metasenv,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
+ let absurd_URI =
+ match LibraryObjects.absurd_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"absurd\" theorem first. Please use the \"default\" command"))
+ in
let ty_term,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
if (ty_term = (C.Sort C.Prop)) (* ma questo controllo serve?? *)
then ProofEngineTypes.apply_tactic
(P.apply_tac
~term:(
- C.Appl [(C.Const (LibraryObjects.absurd_URI (), [] )) ;
+ C.Appl [(C.Const (absurd_URI, [] )) ;
term ; ty])
)
status
let module U = UriManager in
let module P = PrimitiveTactics in
let module T = Tacticals in
+ let false_URI =
+ match LibraryObjects.false_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command"))
+ in
try
ProofEngineTypes.apply_tactic (
T.then_
~continuation:(
T.then_
~start:
- (EliminationTactics.elim_type_tac
- (C.MutInd (LibraryObjects.false_URI (), 0, [])))
+ (EliminationTactics.elim_type_tac (C.MutInd (false_URI, 0, [])))
~continuation: VariousTactics.assumption_tac))
status
with
let refl_proof ty term =
Cic.Appl
[Cic.MutConstruct
- (LibraryObjects.eq_URI (), 0, 1, []);
+ (Utils.eq_URI (), 0, 1, []);
ty; term]
;;
exception TermIsNotAnEquality;;
let term_is_equality term =
- let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+ let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
match term with
| Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
| _ -> false
;;
let equality_of_term proof term =
- let eq_uri = LibraryObjects.eq_URI () in
+ let eq_uri = Utils.eq_URI () in
let iseq uri = UriManager.eq uri eq_uri in
match term with
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
let argsno = List.length menv in
let t =
CicSubstitution.lift argsno
- (Cic.Appl [Cic.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right])
+ (Cic.Appl [Cic.MutInd (Utils.eq_URI (), 0, []); ty; left; right])
in
snd (
List.fold_right
let name = C.Name "x" in
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
+ C.Appl [C.MutInd (Utils.eq_URI (), 0, []);
S.lift 1 eq_ty; l; r]
in
bo',
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
- let eq_uri = LibraryObjects.eq_URI () in
+ let eq_uri = Utils.eq_URI () in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let ok_types ty menv =
List.for_all (fun (_, _, mt) -> mt = ty) menv
eqs)
in
let eq_uri1 = eq_XURI ()
- and eq_uri2 = LibraryObjects.eq_URI () in
+ and eq_uri2 = Utils.eq_URI () in
let iseq uri =
(UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
in
*)
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
- when UriManager.eq uri (LibraryObjects.eq_URI ()) ->
+ when UriManager.eq uri (Utils.eq_URI ()) ->
(let goal_equation =
Equality.mk_equality
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv)
(* in *)
let ok, proof =
(* apply_goal_to_theorems dbd env theorems ~passive active goals in *)
- let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ()) in
+ let iseq uri = UriManager.eq uri (Utils.eq_URI ()) in
match fst goals with
| (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])::_
when left = right && iseq uri ->
(given_clause_fullred dbd env goals theorems passive) active
*)
-let iseq uri = UriManager.eq uri (LibraryObjects.eq_URI ());;
+let iseq uri = UriManager.eq uri (Utils.eq_URI ());;
let check_if_goal_is_identity env = function
| (goalproof,m,Cic.Appl[Cic.MutInd(uri,_,ens);eq_ty;left;right])
context_hyp @ thms, []
else
let refl_equal =
- let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ let us = UriManager.string_of_uri (Utils.eq_URI ()) in
UriManager.uri_of_string (us ^ "#xpointer(1/1/1)")
in
let t = CicUtil.term_of_uri refl_equal in
| Right -> "Right"
;;
-
-let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(LibraryObjects.eq_URI ())
-let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(LibraryObjects.eq_URI ())
-let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let eq_URI () =
+ match LibraryObjects.eq_URI () with
+ None -> assert false
+ | Some uri -> uri
+
+let eq_ind_URI () = LibraryObjects.eq_ind_URI ~eq:(eq_URI ())
+let eq_ind_r_URI () = LibraryObjects.eq_ind_r_URI ~eq:(eq_URI ())
+let sym_eq_URI () = LibraryObjects.sym_eq_URI ~eq:(eq_URI ())
let eq_XURI () =
- let s = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
+ let s = UriManager.string_of_uri (eq_URI ()) in
UriManager.uri_of_string (s ^ "#xpointer(1/1/1)")
-let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(LibraryObjects.eq_URI ())
+let trans_eq_URI () = LibraryObjects.trans_eq_URI ~eq:(eq_URI ())
let metas_of_term t =
List.map fst (CicUtil.metas_of_term t)
val debug_print: string Lazy.t -> unit
+val eq_URI: unit -> UriManager.uri
val eq_ind_URI: unit -> UriManager.uri
val eq_ind_r_URI: unit -> UriManager.uri
val sym_eq_URI: unit -> UriManager.uri
set "baseuri" "cic:/matita/legacy/coq/".
+default "equality"
+ cic:/Coq/Init/Logic/eq.ind
+ cic:/Coq/Init/Logic/sym_eq.con
+ cic:/Coq/Init/Logic/trans_eq.con
+ cic:/Coq/Init/Logic/eq_ind.con
+ cic:/Coq/Init/Logic/eq_ind_r.con.
+
+default "true"
+ cic:/Coq/Init/Logic/True.ind.
+default "false"
+ cic:/Coq/Init/Logic/False.ind.
+default "absurd"
+ cic:/Coq/Init/Logic/absurd.con.
+
(* aritmetic operators *)
interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
projects / helm.git / commitdiff