From: Enrico Tassi Date: Tue, 5 Sep 2006 15:48:19 +0000 (+0000) Subject: fixed coercions. composite can't occur if to funclass X-Git-Tag: make_still_working~6938 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=456f7d82d3cf6732daa36bb07d06c23c4a60beda;p=helm.git fixed coercions. composite can't occur if to funclass --- diff --git a/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml index 798c38540..bd8e992d0 100644 --- a/helm/software/components/cic_unification/cicRefine.ml +++ b/helm/software/components/cic_unification/cicRefine.ml @@ -34,8 +34,8 @@ exception AssertFailure of string Lazy.t;; let insert_coercions = ref true let pack_coercions = ref true -let debug_print = fun _ -> () -(* let debug_print x = prerr_endline (Lazy.force x);; *) +(* let debug_print = fun _ -> () *) + let debug_print x = prerr_endline (Lazy.force x);; let profiler_eat_prods2 = HExtlib.profile "CicRefine.fo_unif_eat_prods2" @@ -144,12 +144,17 @@ let is_a_double_coercion t = | _ -> dummyres) | _ -> dummyres -let more_args_than_expected subst he context hetype' tlbody_and_type = - lazy ("The term " ^ - CicMetaSubst.ppterm_in_context subst he context ^ - " (that has type " ^ CicMetaSubst.ppterm_in_context subst hetype' context ^ - ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ - " arguments that are more than expected") +let more_args_than_expected + localization_tbl subst he context hetype' tlbody_and_type exn += + let msg = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst he context ^ + " (that has type "^CicMetaSubst.ppterm_in_context subst hetype' context ^ + ") is here applied to " ^ string_of_int (List.length tlbody_and_type) ^ + " arguments that are more than expected") + in + enrich localization_tbl he ~f:(fun _-> msg) exn ;; let mk_prod_of_metas metasenv context' subst args = @@ -1248,7 +1253,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t debug_print (lazy ("#### Coercion not packed: " ^ CicPp.ppterm t)); t, ty, subst, metasenv, ugraph) - | _ -> assert false) (* the composite coercion must exist *) + | _ -> t, ty, subst, metasenv, ugraph) else t, ty, subst, metasenv, ugraph @@ -1286,8 +1291,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t let metasenv = pristinemenv in debug_print (lazy ("Fixing arity of: "^CicMetaSubst.ppterm subst hetype ^ - " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' ^ - " cause: " ^ Lazy.force s)); + " since unif failed with: " ^ CicMetaSubst.ppterm subst hetype' + (* ^ " cause: " ^ Lazy.force s *))); let how_many_args_are_needed = let rec aux n = function | Cic.Prod(_,_,t) -> aux (n+1) t @@ -1353,22 +1358,21 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t metasenv context subst t tty remainder ugraph in Some (subst,metasenv,ugraph,hetype',he,args_bo_and_ty) - with exn -> None - with exn -> None) + with Uncertain _ | RefineFailure _ -> None + with Uncertain _ | RefineFailure _ -> None) candidates with | Some(subst,metasenv,ugraph,hetype',he,args_bo_and_ty)-> subst,metasenv,ugraph,hetype',he,args_bo_and_ty | None -> - enrich localization_tbl he - ~f:(fun _-> more_args_than_expected subst he context hetype - args_bo_and_ty) exn + more_args_than_expected localization_tbl + subst he context hetype args_bo_and_ty exn (* }}} end coercion to funclass stuff *) (* }}} end fix_arity *) in (* aux function to process the type of the head and the args in parallel *) let rec eat_prods_and_args - pristinemenv metasenv subst context he hetype ugraph newargs + pristinemenv metasenv subst context pristinehe he hetype ugraph newargs = (* {{{ body *) function @@ -1463,7 +1467,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t "\nReason: " ^ Printexc.to_string exn))) exn (* }}} end coercion stuff *) in - eat_prods_and_args pristinemenv metasenv subst context he + eat_prods_and_args pristinemenv metasenv subst context pristinehe he (CicSubstitution.subst (fst arg) t) ugraph1 (newargs@[arg]) tl | _ -> @@ -1474,14 +1478,11 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t (newargs@[hete,hety]@tl) ugraph in eat_prods_and_args metasenv - metasenv subst context he hetype' ugraph [] args_bo_and_ty - with RefineFailure s | Uncertain s -> + metasenv subst context pristinehe he hetype' ugraph [] args_bo_and_ty + with RefineFailure _ | Uncertain _ as exn -> (* unable to fix arity *) - let msg = - more_args_than_expected - subst he context hetype args_bo_and_ty - in - raise (RefineFailure msg) + more_args_than_expected localization_tbl + subst he context hetype args_bo_and_ty exn (* }}} *) in (* first we check if we are in the simple case of a meta closed term *) @@ -1495,7 +1496,7 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t in let coerced_args,subst,metasenv,he,t,ugraph = eat_prods_and_args - metasenv metasenv subst context he hetype' ugraph1 [] args_bo_and_ty + metasenv metasenv subst context he he hetype' ugraph1 [] args_bo_and_ty in he,(List.map fst coerced_args),t,subst,metasenv,ugraph in diff --git a/helm/software/matita/tests/coercions.ma b/helm/software/matita/tests/coercions.ma index dc4e030bd..1d841d16e 100644 --- a/helm/software/matita/tests/coercions.ma +++ b/helm/software/matita/tests/coercions.ma @@ -105,7 +105,8 @@ definition church: nat \to nat \to nat \def times. coercion cic:/matita/tests/coercions/church.con 1. definition mapmult: \forall n:nat.\forall l:listn nat n. nat \to nat \to nat \def - \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat.l m o. + \lambda n:nat.\lambda l:listn nat n.\lambda m,o:nat. + l (m m) o (o o o).