From 6bb370c6e1a036e82315765d6dceb1939c30ed23 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 14 Dec 2006 13:41:38 +0000 Subject: [PATCH] Huge commit: 1. coercGraph.ml* moved from library to cic_unification (where it should have been put in the first place). A few functions that must remain in library moved to coercDb.ml* (where they should have been put in the first place) 2. ProofEngineHelpers.saturate_term moved from tactic to cic_unification. 3. Bug fixed in saturate_term: the newmeta returned by the function was not correct in some cases 4. CoercGraph.look_for_coercion* used to saturate the coercion with implicit arguments (thus requirin a refinement pass later on). Now the same functions saturate the term with metas. The return type has changed accordingly. 5. the horrible hack to break composite coercions during unification has been replaced by a nice implementation of unification towards the join of the two coercions (called meet by Enrico I do not know why :-). This solves many many problems found using multiple coercion pathes from a source to a destination. (This is the case in DAMA that I am going to commit soon). --- components/acic_content/acic2content.ml | 2 +- components/acic_content/termAcicContent.ml | 4 +- components/cic_unification/.depend | 18 ++- components/cic_unification/Makefile | 2 + components/cic_unification/cicRefine.ml | 79 +++++----- components/cic_unification/cicUnification.ml | 138 ++++++++++++------ .../coercGraph.ml | 65 +++------ .../coercGraph.mli | 14 +- components/cic_unification/termUtil.ml | 89 +++++++++++ components/cic_unification/termUtil.mli | 36 +++++ components/library/.depend | 11 +- components/library/Makefile | 1 - components/library/coercDb.ml | 28 +++- components/library/coercDb.mli | 2 + components/library/librarySync.ml | 2 +- components/tactics/auto.ml | 6 +- components/tactics/equalityTactics.ml | 2 +- components/tactics/primitiveTactics.ml | 4 +- components/tactics/proofEngineHelpers.ml | 63 -------- components/tactics/proofEngineHelpers.mli | 10 -- components/tactics/universe.ml | 2 +- 21 files changed, 337 insertions(+), 241 deletions(-) rename components/{library => cic_unification}/coercGraph.ml (80%) rename components/{library => cic_unification}/coercGraph.mli (75%) create mode 100644 components/cic_unification/termUtil.ml create mode 100644 components/cic_unification/termUtil.mli diff --git a/components/acic_content/acic2content.ml b/components/acic_content/acic2content.ml index 23d644786..a2e7622ea 100644 --- a/components/acic_content/acic2content.ml +++ b/components/acic_content/acic2content.ml @@ -805,7 +805,7 @@ and coercion seed li ~ids_to_inner_types ~ids_to_inner_sorts = | ((Cic.AConst _) as he)::tl | ((Cic.AMutInd _) as he)::tl | ((Cic.AMutConstruct _) as he)::tl when - CoercGraph.is_a_coercion (Deannotate.deannotate_term he) && + CoercDb.is_a_coercion' (Deannotate.deannotate_term he) && !hide_coercions -> let rec last = function diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml index cda76ce09..622a81618 100644 --- a/components/acic_content/termAcicContent.ml +++ b/components/acic_content/termAcicContent.ml @@ -141,9 +141,9 @@ let ast_of_acic0 term_info acic k = | l -> idref aid (Ast.Appl l) in let deannot_he = Deannotate.deannotate_term he in - if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions + if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions then - match CoercGraph.is_a_coercion_to_funclass deannot_he with + match CoercDb.is_a_coercion_to_funclass deannot_he with | None -> idref aid (last_n 1 (List.map k tl)) | Some i -> idref aid (last_n (i+1) (List.map k tl)) else diff --git a/components/cic_unification/.depend b/components/cic_unification/.depend index a442c1d4d..8a34e7deb 100644 --- a/components/cic_unification/.depend +++ b/components/cic_unification/.depend @@ -1,10 +1,16 @@ +termUtil.cmo: cicMkImplicit.cmi termUtil.cmi +termUtil.cmx: cicMkImplicit.cmx termUtil.cmi +coercGraph.cmo: coercGraph.cmi +coercGraph.cmx: coercGraph.cmi cicMetaSubst.cmo: cicMetaSubst.cmi cicMetaSubst.cmx: cicMetaSubst.cmi cicMkImplicit.cmo: cicMkImplicit.cmi cicMkImplicit.cmx: cicMkImplicit.cmi -cicUnification.cmo: cicMetaSubst.cmi cicUnification.cmi -cicUnification.cmx: cicMetaSubst.cmx cicUnification.cmi -cicRefine.cmo: cicUnification.cmi cicMkImplicit.cmi cicMetaSubst.cmi \ - cicRefine.cmi -cicRefine.cmx: cicUnification.cmx cicMkImplicit.cmx cicMetaSubst.cmx \ - cicRefine.cmi +cicUnification.cmo: coercGraph.cmi cicMkImplicit.cmi cicMetaSubst.cmi \ + cicUnification.cmi +cicUnification.cmx: coercGraph.cmx cicMkImplicit.cmx cicMetaSubst.cmx \ + cicUnification.cmi +cicRefine.cmo: coercGraph.cmi cicUnification.cmi cicMkImplicit.cmi \ + cicMetaSubst.cmi cicRefine.cmi +cicRefine.cmx: coercGraph.cmx cicUnification.cmx cicMkImplicit.cmx \ + cicMetaSubst.cmx cicRefine.cmi diff --git a/components/cic_unification/Makefile b/components/cic_unification/Makefile index 62be3a61c..d0c259b27 100644 --- a/components/cic_unification/Makefile +++ b/components/cic_unification/Makefile @@ -4,6 +4,8 @@ PREDICATES = INTERFACE_FILES = \ cicMetaSubst.mli \ cicMkImplicit.mli \ + termUtil.mli \ + coercGraph.mli \ cicUnification.mli \ cicRefine.mli IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index d10e177d0..4fc9f4ccc 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -136,9 +136,9 @@ let is_a_double_coercion t = let imp = Cic.Implicit None in let dummyres = false,imp, imp,imp,imp in match t with - | Cic.Appl (c1::tl) when CoercGraph.is_a_coercion c1 -> + | Cic.Appl (c1::tl) when CoercDb.is_a_coercion' c1 -> (match last_of tl with - | sib1,Cic.Appl (c2::tl2) when CoercGraph.is_a_coercion c2 -> + | sib1,Cic.Appl (c2::tl2) when CoercDb.is_a_coercion' c2 -> let sib2,head = last_of tl2 in true, c1, c2, head,Cic.Appl (c1::sib1@[Cic.Appl (c2::sib2@[imp])]) @@ -324,18 +324,14 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let module C = Cic in let module S = CicSubstitution in let module U = UriManager in - let try_coercion t subst metasenv context ugraph coercion_tgt c = - let coerced = - match c with - C.Appl l2 -> C.Appl (l2@[t]) - | _ -> C.Appl [c;t] + let try_coercion t subst context ugraph coercion_tgt (metasenv,last,coerced) = + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last t ugraph in try - let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context coerced ugraph - in let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context subst metasenv ugraph newt coercion_tgt + avoid_double_coercion context subst metasenv ugraph coerced + coercion_tgt in Some (newt, tty, subst, metasenv, ugraph) with @@ -452,7 +448,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | term -> let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt + CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt in (match boh with | CoercGraph.NoCoercion @@ -475,8 +471,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (try_coercion - t subst metasenv context ugraph coercion_tgt) + (try_coercion t subst context ugraph coercion_tgt) candidates in match selected with @@ -526,7 +521,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | coercion_src -> let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in let boh = - CoercGraph.look_for_coercion coercion_src coercion_tgt + CoercGraph.look_for_coercion metasenv subst context coercion_src coercion_tgt in match boh with | CoercGraph.NoCoercion @@ -549,9 +544,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (try_coercion - s' subst' metasenv' context ugraph1 coercion_tgt) - candidates + (try_coercion s' subst' context ugraph1 coercion_tgt) + candidates in match selected with | Some x -> x @@ -1204,29 +1198,27 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il if b then let source_carr = CoercGraph.source_of c2 in let tgt_carr = CicMetaSubst.apply_subst subst ty in - (match CoercGraph.look_for_coercion source_carr tgt_carr + (match CoercGraph.look_for_coercion metasenv subst context source_carr tgt_carr with | CoercGraph.SomeCoercion candidates -> - let selected = + let selected = HExtlib.list_findopt - (function + (function (metasenv,last,c) -> + match c with | c when not (CoercGraph.is_composite c) -> debug_print (lazy ("\nNot a composite.."^CicPp.ppterm c)); None | c -> - let newt = - match c with - | Cic.Appl l -> Cic.Appl (l @ [head]) - | _ -> Cic.Appl [c;head] - in - debug_print (lazy ("\nprovo" ^ CicPp.ppterm newt)); + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last head ugraph in + debug_print (lazy ("\nprovo" ^ CicPp.ppterm c)); (try debug_print (lazy ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm c)); let newt,_,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in + type_of_aux subst metasenv context c ugraph in debug_print (lazy "tipa..."); let subst, metasenv, ugraph = (* COME MAI C'ERA UN IF su !pack_coercions ??? *) @@ -1346,21 +1338,22 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il CoercDb.coerc_carr_of_term (CicMetaSubst.apply_subst subst xty) in let carr_tgt = CoercDb.Fun 0 in - match CoercGraph.look_for_coercion' carr_src carr_tgt with + match CoercGraph.look_for_coercion' metasenv subst context carr_src carr_tgt with | CoercGraph.NoCoercion | CoercGraph.NotMetaClosed | CoercGraph.NotHandled _ -> raise exn | CoercGraph.SomeCoercion candidates -> match HExtlib.list_findopt - (fun coerc -> - let t = Cic.Appl [coerc;x] in - debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst t)); + (fun (metasenv,last,coerc) -> + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last x ugraph in + debug_print (lazy ("Tentative " ^ CicMetaSubst.ppterm ~metasenv subst coerc)); try (* we want this to be available in the error handler fo the * following (so it has its own try. *) let t,tty,subst,metasenv,ugraph = - type_of_aux subst metasenv context t ugraph + type_of_aux subst metasenv context coerc ugraph in try let metasenv, hetype' = @@ -1386,8 +1379,12 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) with Uncertain _ | RefineFailure _ -> None - with Uncertain _ | RefineFailure _ -> None - | exn -> assert false) (* ritornare None, e' un localized *) + with + Uncertain _ + | RefineFailure _ + | HExtlib.Localized (_,Uncertain _) + | HExtlib.Localized (_,RefineFailure _) -> None + | exn -> assert false) (* ritornare None, e' un localized *) candidates with | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> @@ -1425,7 +1422,7 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il in let c_hety = carr hety subst context in let c_s = carr s subst context in - CoercGraph.look_for_coercion c_hety c_s, c_s + CoercGraph.look_for_coercion metasenv subst context c_hety c_s, c_s in (match coer with | CoercGraph.NoCoercion @@ -1452,12 +1449,14 @@ prerr_endline ("poco geniale: nel caso di IRL basterebbe sapere che questo e' il | CoercGraph.SomeCoercion candidates -> let selected = HExtlib.list_findopt - (fun c -> + (fun (metasenv,last,c) -> try - let t = Cic.Appl[c;hete] in + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv last hete + ugraph in let newt,newhety,subst,metasenv,ugraph = type_of_aux subst metasenv context - t ugraph + c ugraph in let newt, newty, subst, metasenv, ugraph = avoid_double_coercion context subst metasenv diff --git a/components/cic_unification/cicUnification.ml b/components/cic_unification/cicUnification.ml index 86f280842..bcae08df8 100644 --- a/components/cic_unification/cicUnification.ml +++ b/components/cic_unification/cicUnification.ml @@ -593,55 +593,97 @@ debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (match l1, l2 with | (((Cic.Const (uri1, ens1)) as c1) :: tl1), (((Cic.Const (uri2, ens2)) as c2) :: tl2) when - CoercGraph.is_a_coercion c1 && - CoercGraph.is_a_coercion c2 && + CoercDb.is_a_coercion' c1 && + CoercDb.is_a_coercion' c2 && not (UriManager.eq uri1 uri2) -> - let body1, attrs1, ugraph = - match CicEnvironment.get_obj ugraph uri1 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo,attrs,u - | _ -> assert false - in - let body2, attrs2, ugraph = - match CicEnvironment.get_obj ugraph uri2 with - | Cic.Constant (_,Some bo, _, _, attrs),u -> bo, attrs,u - | _ -> assert false - in - let is_composite1 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs1 - in - let is_composite2 = - List.exists - (function `Class (`Coercion _) -> true | _-> false) - attrs2 - in - (match is_composite1, is_composite2 with - | false, false -> raise exn - | true, false -> - let body1 = CicSubstitution.subst_vars ens1 body1 in - let appl = Cic.Appl (body1::tl1) in - let redappl = CicReduction.head_beta_reduce appl in - fo_unif_subst - test_equality_only subst context metasenv - redappl t2 ugraph - | false, true -> - let body2 = CicSubstitution.subst_vars ens2 body2 in - let appl = Cic.Appl (body2::tl2) in - let redappl = CicReduction.head_beta_reduce appl in - fo_unif_subst - test_equality_only subst context metasenv - t1 redappl ugraph - | true, true -> - let body1 = CicSubstitution.subst_vars ens1 body1 in - let appl1 = Cic.Appl (body1::tl1) in - let redappl1 = CicReduction.head_beta_reduce appl1 in - let body2 = CicSubstitution.subst_vars ens2 body2 in - let appl2 = Cic.Appl (body2::tl2) in - let redappl2 = CicReduction.head_beta_reduce appl2 in - fo_unif_subst - test_equality_only subst context metasenv - redappl1 redappl2 ugraph) +(*DEBUGGING ONLY: +prerr_endline ("<<<< " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +let res = +*) + let rec look_for_first_coercion c tl = + match + CicMetaSubst.apply_subst subst (HExtlib.list_last tl) + with + Cic.Appl ((Cic.Const (uri1,ens1) as c')::tl') + when CoercDb.is_a_coercion' c' -> + look_for_first_coercion c' tl' + | last_tl -> c,last_tl + in + let c1,last_tl1 = look_for_first_coercion c1 tl1 in + let c2,last_tl2 = look_for_first_coercion c2 tl2 in + let car1 = + CoercDb.coerc_carr_of_term (CoercGraph.source_of c1) in + let car2 = + CoercDb.coerc_carr_of_term (CoercGraph.source_of c2) in + if CoercDb.eq_carr car1 car2 then + (match last_tl1,last_tl2 with + C.Meta (i1,_),C.Meta(i2,_) when i1=i2 -> raise exn + | C.Meta _, _ + | _, C.Meta _ -> + let subst,metasenv,ugraph = + fo_unif_subst test_equality_only subst context + metasenv last_tl1 last_tl2 ugraph + in + fo_unif_subst test_equality_only subst context + metasenv (C.Appl l1) (C.Appl l2) ugraph + | _ -> raise exn) + else + let meets = CoercGraph.meets car1 car2 in + (match meets with + | [] -> raise exn + | _::_::_ -> +prerr_endline ("1: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); +assert false + | [m] -> + let last_tl1',(subst,metasenv,ugraph) = + match last_tl1 with + | Cic.Meta (i1,l1) + when not (CoercDb.eq_carr m car1) -> + (match + CoercGraph.look_for_coercion' metasenv subst + context m car1 + with + | CoercGraph.SomeCoercion [metasenv,last,coerced] + -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl1 ugraph + | _ -> +prerr_endline ("2: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); +assert false) + | _ -> last_tl1,(subst,metasenv,ugraph) in + let last_tl2',(subst,metasenv,ugraph) = + match last_tl2 with + Cic.Meta (i2,l2) when not (CoercDb.eq_carr m car2) -> + (match + CoercGraph.look_for_coercion' metasenv subst + context m car2 + with + | CoercGraph.SomeCoercion [metasenv,last,coerced] + -> + last, + fo_unif_subst test_equality_only subst context + metasenv coerced last_tl2 ugraph + | _ -> +prerr_endline ("3: NON DOVEVA SUCCEDERE!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); +assert false) + | _ -> last_tl2,(subst,metasenv,ugraph) + in +(*DEBUGGING ONLY: +prerr_endline ("OK " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl1' context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst last_tl2' context); +*) + let subst,metasenv,ugraph = + fo_unif_subst test_equality_only subst context + metasenv last_tl1' last_tl2' ugraph + in + fo_unif_subst test_equality_only subst context + metasenv (C.Appl l1) (C.Appl l2) ugraph) +(*DEBUGGING ONLY: +in +let subst,metasenv,ugraph = res in +prerr_endline (">>>> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l1) context ^ " <==> " ^ CicMetaSubst.ppterm_in_context ~metasenv subst (C.Appl l2) context); +res +*) (*CSC: This is necessary because of the "elim H" tactic where the type of H is only reducible to an inductive type. This could be extended from inductive diff --git a/components/library/coercGraph.ml b/components/cic_unification/coercGraph.ml similarity index 80% rename from components/library/coercGraph.ml rename to components/cic_unification/coercGraph.ml index 355c8019a..70e90af52 100644 --- a/components/library/coercGraph.ml +++ b/components/cic_unification/coercGraph.ml @@ -28,7 +28,10 @@ open Printf;; type coercion_search_result = - | SomeCoercion of Cic.term list + (* metasenv, last coercion argument, fully saturated coercion *) + (* to apply the coercion it is sufficient to unify the last coercion + argument (that is a Meta) with the term to be coerced *) + | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t @@ -37,21 +40,7 @@ let debug = false let debug_print s = if debug then prerr_endline (Lazy.force s) else () (* searches a coercion fron src to tgt in the !coercions list *) -let look_for_coercion' src tgt = - let arity_of con = - try - let ty,_ = CicTypeChecker.type_of_aux' [] [] con CicUniv.empty_ugraph in - let rec count_pi = function - | Cic.Prod (_,_,t) -> 1 + count_pi t - | _ -> 0 - in - count_pi ty - with Invalid_argument _ -> assert false (* all coercions have an uri *) - in - let rec mk_implicits = function - | 0 -> [] - | n -> Cic.Implicit None :: mk_implicits (n-1) - in +let look_for_coercion' metasenv subst context src tgt = try let l = CoercDb.find_coercion @@ -81,19 +70,23 @@ let look_for_coercion' src tgt = let _,tgtcarl = List.split (List.map CoercDb.get_carr ul) in List.map (function CoercDb.Fun i -> i | _ -> 0) tgtcarl in - let arityl = List.map arity_of cl in - let argsl = - List.map2 - (fun arity fn_arity -> - mk_implicits (arity - 1 - fn_arity)) arityl funclass_arityl - in + let freshmeta = CicMkImplicit.new_meta metasenv subst in let newtl = - List.map2 - (fun args c -> + List.map2 + (fun arity c -> + let ty,_ = + CicTypeChecker.type_of_aux' ~subst metasenv context c + CicUniv.empty_ugraph in + let _,metasenv,args,lastmeta = + TermUtil.saturate_term freshmeta metasenv context ty arity in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + metasenv, Cic.Meta (lastmeta-1,irl), match args with - | [] -> c - | _ -> Cic.Appl (c::args)) - argsl cl + [] -> c + | _ -> Cic.Appl (c::args) + ) funclass_arityl cl in SomeCoercion newtl) with @@ -101,16 +94,10 @@ let look_for_coercion' src tgt = | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed ;; -let look_for_coercion src tgt = +let look_for_coercion metasenv subst context src tgt = let src_uri = CoercDb.coerc_carr_of_term src in let tgt_uri = CoercDb.coerc_carr_of_term tgt in - look_for_coercion' src_uri tgt_uri - -let is_a_coercion t = - try - let uri = CicUtil.uri_of_term t in - CoercDb.is_a_coercion uri - with Invalid_argument _ -> false + look_for_coercion' metasenv subst context src_uri tgt_uri let source_of t = try @@ -118,14 +105,6 @@ let source_of t = CoercDb.term_of_carr (fst (CoercDb.get_carr uri)) with Invalid_argument _ -> assert false (* t must be a coercion *) -let is_a_coercion_to_funclass t = - try - let uri = CicUtil.uri_of_term t in - match snd (CoercDb.get_carr uri) with - | CoercDb.Fun i -> Some i - | _ -> None - with Invalid_argument _ -> None - let generate_dot_file () = let module Pp = GraphvizPp.Dot in let buf = Buffer.create 10240 in diff --git a/components/library/coercGraph.mli b/components/cic_unification/coercGraph.mli similarity index 75% rename from components/library/coercGraph.mli rename to components/cic_unification/coercGraph.mli index e6bc766df..62e484499 100644 --- a/components/library/coercGraph.mli +++ b/components/cic_unification/coercGraph.mli @@ -28,19 +28,21 @@ (* This module implements the Query interface to the Coercion Graph *) type coercion_search_result = - | SomeCoercion of Cic.term list + (* metasenv, last coercion argument, fully saturated coercion *) + (* to apply the coercion it is sufficient to unify the last coercion + argument (that is a Meta) with the term to be coerced *) + | SomeCoercion of (Cic.metasenv * Cic.term * Cic.term) list | NoCoercion | NotMetaClosed | NotHandled of string Lazy.t val look_for_coercion : - Cic.term -> Cic.term -> coercion_search_result + Cic.metasenv -> Cic.substitution -> Cic.context -> + Cic.term -> Cic.term -> coercion_search_result val look_for_coercion' : - CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result - -val is_a_coercion: Cic.term -> bool -val is_a_coercion_to_funclass: Cic.term -> int option + Cic.metasenv -> Cic.substitution -> Cic.context -> + CoercDb.coerc_carr -> CoercDb.coerc_carr -> coercion_search_result (* checks if term is a constant or * a constant applyed that is marked with (`Class `Coercion) *) diff --git a/components/cic_unification/termUtil.ml b/components/cic_unification/termUtil.ml new file mode 100644 index 000000000..8905830be --- /dev/null +++ b/components/cic_unification/termUtil.ml @@ -0,0 +1,89 @@ +(* Copyright (C) 2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *) + +(* saturate_term newmeta metasenv context ty goal_arity *) +(* Given a type [ty] (a backbone), it returns its suffix of length *) +(* [goal_arity] head and a new metasenv in which there is new a META for each *) +(* hypothesis, a list of arguments for the new applications and the index of *) +(* the last new META introduced. The nth argument in the list of arguments is *) +(* just the nth new META. *) +let saturate_term newmeta metasenv context ty goal_arity = + let module C = Cic in + let module S = CicSubstitution in + assert (goal_arity >= 0); + let rec aux newmeta ty = + match ty with + C.Cast (he,_) -> aux newmeta he +(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type + (* If the expected type is a Type, then also Set is OK ==> + * we accept any term of type Type *) + (*CSC: BUG HERE: in this way it is possible for the term of + * type Type to be different from a Sort!!! *) + | C.Prod (name,(C.Sort (C.Type _) as s),t) -> + (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let newargument = C.Meta (newmeta+1,irl) in + let (res,newmetasenv,arguments,lastmeta) = + aux (newmeta + 2) (S.subst newargument t) + in + res, + (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, + newargument::arguments,lastmeta +*) + | C.Prod (name,s,t) -> + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context + in + let newargument = C.Meta (newmeta,irl) in + let res,newmetasenv,arguments,lastmeta,prod_no = + aux (newmeta + 1) (S.subst newargument t) + in + if prod_no + 1 = goal_arity then + let head = CicReduction.normalize ~delta:false context ty in + head,[],[],newmeta,goal_arity + 1 + else + (** NORMALIZE RATIONALE + * we normalize the target only NOW since we may be in this case: + * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k + * and we want a mesasenv with ?1:A1 and ?2:A2 and not + * ?1, ?2, ?3 (that is the one we whould get if we start from the + * beta-normalized A1 -> A2 -> A3 -> P **) + let s' = CicReduction.normalize ~delta:false context s in + res,(newmeta,context,s')::newmetasenv,newargument::arguments, + lastmeta,prod_no + 1 + | t -> + let head = CicReduction.normalize ~delta:false context t in + match CicReduction.whd context head with + C.Prod _ as head' -> aux newmeta head' + | _ -> head,[],[],newmeta,0 + in + (* WARNING: here we are using the invariant that above the most *) + (* recente new_meta() there are no used metas. *) + let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in + res,metasenv @ newmetasenv,arguments,lastmeta diff --git a/components/cic_unification/termUtil.mli b/components/cic_unification/termUtil.mli new file mode 100644 index 000000000..358b64616 --- /dev/null +++ b/components/cic_unification/termUtil.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000-2002, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + +(* $Id: proofEngineHelpers.ml 7022 2006-11-15 19:47:41Z fguidi $ *) + +(* saturate_term newmeta metasenv context ty goal_arity *) +(* Given a type [ty] (a backbone), it returns its suffix of length *) +(* [goal_arity] head and a new metasenv in which there is new a META for each *) +(* hypothesis, a list of arguments for the new applications and the index of *) +(* the last new META introduced. The nth argument in the list of arguments is *) +(* just the nth new META. *) +val saturate_term: + int -> Cic.metasenv -> Cic.context -> Cic.term -> int -> + Cic.term * Cic.metasenv * Cic.term list * int diff --git a/components/library/.depend b/components/library/.depend index bc1a71311..5f391bc0f 100644 --- a/components/library/.depend +++ b/components/library/.depend @@ -1,5 +1,4 @@ cicCoercion.cmi: refinementTool.cmo coercDb.cmi -coercGraph.cmi: coercDb.cmi librarySync.cmi: refinementTool.cmo cicElim.cmo: cicElim.cmi cicElim.cmx: cicElim.cmi @@ -13,12 +12,10 @@ coercDb.cmo: coercDb.cmi coercDb.cmx: coercDb.cmi cicCoercion.cmo: refinementTool.cmo coercDb.cmi cicCoercion.cmi cicCoercion.cmx: refinementTool.cmx coercDb.cmx cicCoercion.cmi -coercGraph.cmo: coercDb.cmi coercGraph.cmi -coercGraph.cmx: coercDb.cmx coercGraph.cmi -librarySync.cmo: refinementTool.cmo libraryDb.cmi coercGraph.cmi coercDb.cmi \ - cicRecord.cmi cicElim.cmi cicCoercion.cmi librarySync.cmi -librarySync.cmx: refinementTool.cmx libraryDb.cmx coercGraph.cmx coercDb.cmx \ - cicRecord.cmx cicElim.cmx cicCoercion.cmx librarySync.cmi +librarySync.cmo: refinementTool.cmo libraryDb.cmi coercDb.cmi cicRecord.cmi \ + cicElim.cmi cicCoercion.cmi librarySync.cmi +librarySync.cmx: refinementTool.cmx libraryDb.cmx coercDb.cmx cicRecord.cmx \ + cicElim.cmx cicCoercion.cmx librarySync.cmi libraryNoDb.cmo: libraryNoDb.cmi libraryNoDb.cmx: libraryNoDb.cmi libraryClean.cmo: librarySync.cmi libraryNoDb.cmi libraryMisc.cmi \ diff --git a/components/library/Makefile b/components/library/Makefile index 69a10919d..013f5f4a0 100644 --- a/components/library/Makefile +++ b/components/library/Makefile @@ -8,7 +8,6 @@ INTERFACE_FILES = \ libraryDb.mli \ coercDb.mli \ cicCoercion.mli \ - coercGraph.mli \ librarySync.mli \ libraryNoDb.mli \ libraryClean.mli \ diff --git a/components/library/coercDb.ml b/components/library/coercDb.ml index ed3d58c72..2e93efa0e 100644 --- a/components/library/coercDb.ml +++ b/components/library/coercDb.ml @@ -118,12 +118,6 @@ let find_coercion f = (HExtlib.filter_map (fun (s,t,l) -> if f (s,t) then Some l else None) !db)) ;; -let is_a_coercion u = - List.exists - (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) - !db -;; - let get_carr uri = try let src, tgt, _ = @@ -135,6 +129,28 @@ let get_carr uri = with Not_found -> assert false (* uri must be a coercion *) ;; +let is_a_coercion u = + List.exists + (fun (_,_,xl) -> List.exists (fun (x,_) -> UriManager.eq u x) xl) + !db +;; + +let is_a_coercion' t = + try + let uri = CicUtil.uri_of_term t in + is_a_coercion uri + with Invalid_argument _ -> false +;; + +let is_a_coercion_to_funclass t = + try + let uri = CicUtil.uri_of_term t in + match snd (get_carr uri) with + | Fun i -> Some i + | _ -> None + with Invalid_argument _ -> None + + let term_of_carr = function | Uri u -> CicUtil.term_of_uri u | Sort s -> Cic.Sort s diff --git a/components/library/coercDb.mli b/components/library/coercDb.mli index d8a8b0574..5f455c2af 100644 --- a/components/library/coercDb.mli +++ b/components/library/coercDb.mli @@ -60,6 +60,8 @@ val find_coercion: (coerc_carr * coerc_carr -> bool) -> UriManager.uri list val is_a_coercion: UriManager.uri -> bool +val is_a_coercion': Cic.term -> bool +val is_a_coercion_to_funclass: Cic.term -> int option val get_carr: UriManager.uri -> coerc_carr * coerc_carr val term_of_carr: coerc_carr -> Cic.term diff --git a/components/library/librarySync.ml b/components/library/librarySync.ml index 4dc20f77f..d5eca252a 100644 --- a/components/library/librarySync.ml +++ b/components/library/librarySync.ml @@ -111,7 +111,7 @@ let add_single_obj uri obj refinement_toolkit = let module RT = RefinementTool in let obj = if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*) - not (CoercGraph.is_a_coercion (Cic.Const (uri, []))) + not (CoercDb.is_a_coercion' (Cic.Const (uri, []))) then refinement_toolkit.RT.pack_coercion_obj obj else diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml index 3c35013aa..5f110bc4c 100644 --- a/components/tactics/auto.ml +++ b/components/tactics/auto.ml @@ -84,7 +84,7 @@ let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;; let is_unit_equation context metasenv oldnewmeta term = let head, metasenv, args, newmeta = - ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + TermUtil.saturate_term oldnewmeta metasenv context term 0 in let propositional_args = HExtlib.filter_map @@ -246,7 +246,7 @@ let init_cache_and_tables dbd use_library paramod universe (proof, goal) = let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast = let head, metasenv, args, newmeta = - ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + TermUtil.saturate_term oldnewmeta metasenv context term 0 in let propositional_args = HExtlib.filter_map @@ -430,7 +430,7 @@ let new_metasenv_and_unify_and_t context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in + TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in diff --git a/components/tactics/equalityTactics.ml b/components/tactics/equalityTactics.ml index cd066250f..e81f54076 100644 --- a/components/tactics/equalityTactics.ml +++ b/components/tactics/equalityTactics.ml @@ -105,7 +105,7 @@ let rec rewrite_tac ~direction ~(pattern: ProofEngineTypes.lazy_pattern) equalit CicTypeChecker.type_of_aux' metasenv context equality CicUniv.empty_ugraph in let (ty_eq,metasenv',arguments,fresh_meta) = - ProofEngineHelpers.saturate_term + TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in let equality = if List.length arguments = 0 then diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index c9d68d9de..5f8533916 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -231,7 +231,7 @@ let let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = - ProofEngineHelpers.saturate_term newmeta' metasenv' context termty + TermUtil.saturate_term newmeta' metasenv' context termty goal_arity in let subst,newmetasenv',_ = CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph @@ -485,7 +485,7 @@ let elim_tac ~term = let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in let termty = CicReduction.whd context termty in let (termty,metasenv',arguments,fresh_meta) = - ProofEngineHelpers.saturate_term + TermUtil.saturate_term (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty 0 in let term = if arguments = [] then term else Cic.Appl (term::arguments) in let uri,exp_named_subst,typeno,args = diff --git a/components/tactics/proofEngineHelpers.ml b/components/tactics/proofEngineHelpers.ml index b4e9a4e94..9dfad7651 100644 --- a/components/tactics/proofEngineHelpers.ml +++ b/components/tactics/proofEngineHelpers.ml @@ -613,69 +613,6 @@ let locate_in_conjecture ?(equality=fun _ -> (==)) what (_,context,ty) = in res @ locate_in_term what ~where:ty context -(* saturate_term newmeta metasenv context ty goal_arity *) -(* Given a type [ty] (a backbone), it returns its suffix of length *) -(* [goal_arity] head and a new metasenv in which there is new a META for each *) -(* hypothesis, a list of arguments for the new applications and the index of *) -(* the last new META introduced. The nth argument in the list of arguments is *) -(* just the nth new META. *) -let saturate_term newmeta metasenv context ty goal_arity = - let module C = Cic in - let module S = CicSubstitution in - assert (goal_arity >= 0); - let rec aux newmeta ty = - match ty with - C.Cast (he,_) -> aux newmeta he -(* CSC: patch to generate ?1 : ?2 : Type in place of ?1 : Type to simulate ?1 :< Type - (* If the expected type is a Type, then also Set is OK ==> - * we accept any term of type Type *) - (*CSC: BUG HERE: in this way it is possible for the term of - * type Type to be different from a Sort!!! *) - | C.Prod (name,(C.Sort (C.Type _) as s),t) -> - (* TASSI: ask CSC if BUG HERE refers to the C.Cast or C.Propd case *) - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta+1,irl) in - let (res,newmetasenv,arguments,lastmeta) = - aux (newmeta + 2) (S.subst newargument t) - in - res, - (newmeta,[],s)::(newmeta+1,context,C.Meta (newmeta,[]))::newmetasenv, - newargument::arguments,lastmeta -*) - | C.Prod (name,s,t) -> - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let newargument = C.Meta (newmeta,irl) in - let res,newmetasenv,arguments,lastmeta,prod_no = - aux (newmeta + 1) (S.subst newargument t) - in - if prod_no + 1 = goal_arity then - let head = CicReduction.normalize ~delta:false context ty in - head,[],[],lastmeta,goal_arity + 1 - else - (** NORMALIZE RATIONALE - * we normalize the target only NOW since we may be in this case: - * A1 -> A2 -> T where T = (\lambda x.A3 -> P) k - * and we want a mesasenv with ?1:A1 and ?2:A2 and not - * ?1, ?2, ?3 (that is the one we whould get if we start from the - * beta-normalized A1 -> A2 -> A3 -> P **) - let s' = CicReduction.normalize ~delta:false context s in - res,(newmeta,context,s')::newmetasenv,newargument::arguments, - lastmeta,prod_no + 1 - | t -> - let head = CicReduction.normalize ~delta:false context t in - match CicReduction.whd context head with - C.Prod _ as head' -> aux newmeta head' - | _ -> head,[],[],newmeta,0 - in - (* WARNING: here we are using the invariant that above the most *) - (* recente new_meta() there are no used metas. *) - let res,newmetasenv,arguments,lastmeta,_ = aux newmeta ty in - res,metasenv @ newmetasenv,arguments,lastmeta - let lookup_type metasenv context hyp = let rec aux p = function | Some (Cic.Name name, Cic.Decl t) :: _ when name = hyp -> p, t diff --git a/components/tactics/proofEngineHelpers.mli b/components/tactics/proofEngineHelpers.mli index 650271d5e..f0b2c87f1 100644 --- a/components/tactics/proofEngineHelpers.mli +++ b/components/tactics/proofEngineHelpers.mli @@ -103,16 +103,6 @@ val locate_in_conjecture: ?equality:(Cic.context -> Cic.term -> Cic.term -> bool) -> Cic.term -> Cic.conjecture -> (Cic.context * Cic.term) list -(* saturate_term newmeta metasenv context ty goal_arity *) -(* Given a type [ty] (a backbone), it returns its suffix of length *) -(* [goal_arity] head and a new metasenv in which there is new a META for each *) -(* hypothesis, a list of arguments for the new applications and the index of *) -(* the last new META introduced. The nth argument in the list of arguments is *) -(* just the nth new META. *) -val saturate_term: - int -> Cic.metasenv -> Cic.context -> Cic.term -> int -> - Cic.term * Cic.metasenv * Cic.term list * int - (* returns the index and the type of a premise in a context *) val lookup_type: Cic.metasenv -> Cic.context -> string -> int * Cic.term diff --git a/components/tactics/universe.ml b/components/tactics/universe.ml index 40c3c1abd..eeff1fa96 100644 --- a/components/tactics/universe.ml +++ b/components/tactics/universe.ml @@ -57,7 +57,7 @@ let rec collapse_head_metas = function let rec dummies_of_coercions = function - | Cic.Appl (c::l) when CoercGraph.is_a_coercion c -> + | Cic.Appl (c::l) when CoercDb.is_a_coercion' c -> Cic.Meta (-1,[]) | Cic.Appl l -> let l' = List.map dummies_of_coercions l in Cic.Appl l' -- 2.39.2