| Cic.Appl l -> List.for_all is_simple_term l
| Cic.Meta (i, l) -> check_irl 1 l
| Cic.Rel _ -> true
+ | Cic.Const _ -> true
| _ -> false
;;
let module U = CicUnification in
let lookup = lookup_subst in
let rec occurs_check subst what where =
- (* Printf.printf "occurs_check %s %s" *)
- (* (CicPp.ppterm what) (CicPp.ppterm where); *)
- (* print_newline (); *)
match where with
| t when what = t -> true
| C.Appl l -> List.exists (occurs_check subst what) l
| _ -> false
in
let rec unif subst menv s t =
-(* Printf.printf "unif %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *)
-(* (print_subst subst); *)
-(* print_newline (); *)
let s = match s with C.Meta _ -> lookup s subst | _ -> s
and t = match t with C.Meta _ -> lookup t subst | _ -> t
in
- (* Printf.printf "after apply_subst: %s %s\n%s" *)
- (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *)
- (* print_newline (); *)
match s, t with
| s, t when s = t -> subst, menv
| C.Meta (i, _), C.Meta (j, _) when i > j ->
unif subst menv t s
| C.Meta _, t when occurs_check subst s t ->
raise (U.UnificationFailure "Inference.unification.unif")
-(* | C.Meta (i, l), C.Meta (j, l') -> *)
-(* let _, _, ty = CicUtil.lookup_meta i menv in *)
-(* let _, _, ty' = CicUtil.lookup_meta j menv in *)
-(* let binding1 = lookup s subst in *)
-(* let binding2 = lookup t subst in *)
-(* let subst, menv = *)
-(* if binding1 != s then *)
-(* if binding2 != t then *)
-(* unif subst menv binding1 binding2 *)
-(* else *)
-(* if binding1 = t then *)
-(* subst, menv *)
-(* else *)
-(* ((j, (context, binding1, ty'))::subst, *)
-(* List.filter (fun (m, _, _) -> j <> m) menv) *)
-(* else *)
-(* if binding2 != t then *)
-(* if s = binding2 then *)
-(* subst, menv *)
-(* else *)
-(* ((i, (context, binding2, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* else *)
-(* ((i, (context, t, ty))::subst, *)
-(* List.filter (fun (m, _, _) -> i <> m) menv) *)
-(* in *)
-(* subst, menv *)
-
| C.Meta (i, l), t ->
let _, _, ty = CicUtil.lookup_meta i menv in
let subst =
| _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
in
let subst, menv = unif [] metasenv t1 t2 in
- (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *)
- (* print_newline (); *)
-(* let rec fix_term = function *)
-(* | (C.Meta (i, l) as t) -> *)
-(* lookup t subst *)
-(* | C.Appl l -> C.Appl (List.map fix_term l) *)
-(* | t -> t *)
-(* in *)
-(* let rec fix_subst = function *)
-(* | [] -> [] *)
-(* | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) *)
-(* in *)
-(* List.rev (fix_subst subst), menv, ugraph *)
List.rev subst, menv, ugraph
;;
(* (\* print_newline (); *\) *)
(* subst, menv, ug *)
(* else *)
+(* Printf.printf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+(* print_newline (); *)
try
let subst, metasenv, ugraph =
(* CicUnification.fo_unif metasenv context t1 t2 ugraph *)
with e ->
(* Printf.printf "failed to match %s %s\n" *)
(* (CicPp.ppterm t1) (CicPp.ppterm t2); *)
+(* print_endline (Printexc.to_string e); *)
raise MatchingFailure
;;
C.Appl ((C.Rel index)::args)
in (
match head with
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when UriManager.eq uri eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
Some e, (newmeta+1)
| _ -> None, newmeta
)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when UriManager.eq uri eq_uri ->
let t1 = S.lift index t1
and t2 = S.lift index t2 in
let o = !Utils.compare_terms t1 t2 in
;;
-let find_library_equalities ~(dbd:Mysql.dbd) status maxmeta =
+let equations_blacklist =
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
+ UriManager.UriSet.empty [
+ "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+ "cic:/Coq/Init/Logic/trans_eq.con";
+ "cic:/Coq/Init/Logic/f_equal.con";
+ "cic:/Coq/Init/Logic/f_equal2.con";
+ "cic:/Coq/Init/Logic/f_equal3.con";
+ "cic:/Coq/Init/Logic/sym_eq.con"
+ ]
+;;
+
+let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
let candidates =
- List.map
- (fun uri ->
- let t = CicUtil.term_of_uri uri in
- let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
- t, ty)
+ List.fold_left
+ (fun l uri ->
+ if UriManager.UriSet.mem uri equations_blacklist then
+ l
+ else
+ let t = CicUtil.term_of_uri uri in
+ let ty, _ =
+ CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph
+ in
+ (t, ty)::l)
+ []
(MetadataQuery.equations_for_goal ~dbd status)
in
let eq_uri1 = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI
and eq_uri2 = HelmLibraryObjects.Logic.eq_URI in
let iseq uri =
- uri == eq_uri1 || uri == eq_uri2
+ (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
in
let rec aux newmeta = function
| [] -> [], newmeta
match termty with
| C.Prod (name, s, t) ->
let head, newmetas, args, newmeta =
- ProofEngineHelpers.saturate_term newmeta [] [] termty
+ ProofEngineHelpers.saturate_term newmeta [] context termty
in
let p =
if List.length args = 0 then
;;
+let term_is_equality ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) term =
+ let iseq uri = UriManager.eq uri eq_uri in
+ match term with
+ | Cic.Appl [Cic.MutInd (uri, _, _); _; _; _] when iseq uri -> true
+ | _ -> false
+;;
+
+
exception TermIsNotAnEquality;;
-let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
- | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
+let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof term =
+ let iseq uri = UriManager.eq uri eq_uri in
+ match term with
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
let o = !Utils.compare_terms t1 t2 in
let w = compute_equality_weight ty t1 t2 in
let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in
projects / helm.git / blobdiff