From: Claudio Sacerdoti Coen Date: Sat, 18 Feb 2006 15:53:16 +0000 (+0000) Subject: Bug fixed in insertion of parametric coercions. X-Git-Tag: 0.4.95@7852~1654 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=27b3610b7add7ee75eb25f8f01e0f1426c278f52;p=helm.git Bug fixed in insertion of parametric coercions. To fix the bug, the CoercGraph.look_for_coercion now returns a term saturated with Cic.Implicits. As usual, remember to refine the term before further usage. --- diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml index b9c5b0c6a..844260480 100644 --- a/components/cic_unification/cicRefine.ml +++ b/components/cic_unification/cicRefine.ml @@ -118,54 +118,6 @@ let is_a_double_coercion t = | _ -> dummyres) | _ -> dummyres -let avoid_double_coercion context subst metasenv ugraph t ty = - 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 tail = function - | 0 -> [tail] - | n -> Cic.Implicit None :: mk_implicits tail (n-1) - in - let b, c1, c2, head = is_a_double_coercion t in - 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 - with - | CoercGraph.SomeCoercion c -> - let arity = arity_of c in - let args = mk_implicits head (arity - 1) in - let c_bo = CicUtil.term_of_uri (CicUtil.uri_of_term c) in - let newt = Cic.Appl (c_bo::args) in - (try - let subst, metasenv, ugraph = - fo_unif_subst subst context metasenv newt t ugraph - in - debug_print - (lazy - ("packing: " ^ - CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm (Cic.Appl (c::args)))); - Cic.Appl (c::args), ty, subst, metasenv, ugraph - with - RefineFailure _ -> - prerr_endline ("#### Coercion not packed (Refine_failure): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); - assert false - | Uncertain _ -> - prerr_endline ("#### Coercion not packed (Uncercatin case): " ^ - CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm (Cic.Appl (c::args))); - assert false) - | _ -> assert false) (* the composite coercion must exist *) - else - t, ty, subst, metasenv, ugraph - let rec type_of_constant uri ugraph = let module C = Cic in let module R = CicReduction in @@ -395,8 +347,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t t, cast, subst, metasenv, ugraph | term -> let coercion_tgt = carr (Cic.Sort tgt_sort) subst context in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in + let boh = + CoercGraph.look_for_coercion coercion_src coercion_tgt + in (match boh with | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> @@ -416,10 +369,12 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst coercion_src context ^ " that is not a sort"))) | CoercGraph.SomeCoercion c -> + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context (Cic.Appl[c;t]) + ugraph in let newt, tty, subst, metasenv, ugraph = - avoid_double_coercion context - subst metasenv ugraph - (Cic.Appl[c;t]) coercion_tgt + avoid_double_coercion context subst metasenv ugraph + newt coercion_tgt in newt, tty, subst, metasenv, ugraph) in @@ -456,14 +411,17 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t | C.Meta _ | C.Sort _ -> s',sort1, subst', metasenv', ugraph1 | coercion_src -> let coercion_tgt = Cic.Sort (Cic.Type (CicUniv.fresh())) in - let search = CoercGraph.look_for_coercion in - let boh = search coercion_src coercion_tgt in + let boh = + CoercGraph.look_for_coercion coercion_src coercion_tgt + in match boh with | CoercGraph.SomeCoercion c -> + let newt,_,subst',metasenv',ugraph1 = + type_of_aux subst' metasenv' context (Cic.Appl[c;s']) + ugraph1 in let newt, tty, subst', metasenv', ugraph1 = - avoid_double_coercion context - subst' metasenv' ugraph1 - (Cic.Appl[c;s']) coercion_tgt + avoid_double_coercion context subst' metasenv' + ugraph1 newt coercion_tgt in newt, tty, subst', metasenv', ugraph1 | CoercGraph.NoCoercion @@ -1111,6 +1069,43 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2'')))) + and avoid_double_coercion context subst metasenv ugraph t ty = + let b, c1, c2, head = is_a_double_coercion t in + 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 + with + | CoercGraph.SomeCoercion c -> + let newt = + match c with + Cic.Appl l -> Cic.Appl (l @ [head]) + | _ -> Cic.Appl [c;head] + in + (try + let newt,_,subst,metasenv,ugraph = + type_of_aux subst metasenv context newt ugraph in + let subst, metasenv, ugraph = + fo_unif_subst subst context metasenv newt t ugraph + in + debug_print + (lazy + ("packing: " ^ + CicPp.ppterm t ^ " ==> " ^ CicPp.ppterm newt)); + newt, ty, subst, metasenv, ugraph + with + RefineFailure _ -> + prerr_endline ("#### Coercion not packed (Refine_failure): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); + assert false + | Uncertain _ -> + prerr_endline ("#### Coercion not packed (Uncercatin case): " ^ + CicPp.ppterm t ^ " =/=> " ^ CicPp.ppterm newt); + assert false) + | _ -> assert false) (* the composite coercion must exist *) + else + t, ty, subst, metasenv, ugraph + and eat_prods allow_coercions subst metasenv context he hetype tlbody_and_type ugraph = @@ -1216,20 +1211,20 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t CicMetaSubst.ppterm_in_context subst s context (* "\nReason: " ^ Lazy.force e*)))) | CoercGraph.SomeCoercion c -> + try + let newt,newhety,subst,metasenv,ugraph = + type_of_aux subst metasenv context + (Cic.Appl[c;hete]) ugraph in let newt, _, subst, metasenv, ugraph = - avoid_double_coercion context - subst metasenv ugraph - (Cic.Appl[c;hete]) tgt_carr in - try - let newty,newhety,subst,metasenv,ugraph = - type_of_aux subst metasenv context newt ugraph in + avoid_double_coercion context subst metasenv + ugraph newt tgt_carr in let subst,metasenv,ugraph1 = fo_unif_subst subst context metasenv newhety s ugraph in newt, subst, metasenv, ugraph - with _ -> - enrich localization_tbl hete + with _ -> + enrich localization_tbl hete ~f:(fun _ -> (lazy ("The term " ^ CicMetaSubst.ppterm_in_context subst hete diff --git a/components/library/coercGraph.ml b/components/library/coercGraph.ml index 62a89b0a7..06d7a12d3 100644 --- a/components/library/coercGraph.ml +++ b/components/library/coercGraph.ml @@ -38,34 +38,61 @@ 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 try let l = CoercDb.find_coercion - (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) + (fun (s,t) -> CoercDb.eq_carr s src && CoercDb.eq_carr t tgt) in + let uri = + match l with + | [] -> + debug_print + (lazy + (sprintf ":-( coercion non trovata da %s a %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt))); + None + | [u] -> + debug_print (lazy ( + sprintf ":-) TROVATA 1 coercion da %s a %s: %s" + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt) + (UriManager.name_of_uri u))); + Some u + | u::_ -> + debug_print (lazy ( + sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" + (List.length l) + (CoercDb.name_of_carr src) + (CoercDb.name_of_carr tgt) + (UriManager.name_of_uri u))); + Some u in - match l with - | [] -> - debug_print - (lazy - (sprintf ":-( coercion non trovata da %s a %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt))); - NoCoercion - | [u] -> - debug_print (lazy ( - sprintf ":-) TROVATA 1 coercion da %s a %s: %s" - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - SomeCoercion (CicUtil.term_of_uri u) - | u::_ -> - debug_print (lazy ( - sprintf ":-/ TROVATE %d coercion(s) da %s a %s, prendo la prima: %s" - (List.length l) - (CoercDb.name_of_carr src) - (CoercDb.name_of_carr tgt) - (UriManager.name_of_uri u))); - SomeCoercion (CicUtil.term_of_uri u) + (match uri with + None -> NoCoercion + | Some u -> + let c = CicUtil.term_of_uri u in + let arity = arity_of c in + let args = mk_implicits (arity - 1) in + let newt = + match args with + [] -> c + | _ -> Cic.Appl (c::args) + in + SomeCoercion newt) with | CoercDb.EqCarrNotImplemented s -> NotHandled s | CoercDb.EqCarrOnNonMetaClosed -> NotMetaClosed