X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicRefine.ml;h=d3a297d43e88b517cec0e9caf4eef32e322896d9;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=03acb40cb7b7b3c59958b8706a2273b528140bd3;hpb=8523a35427aa3fdf40a0e14b8aac3428c8aa13f0;p=helm.git diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 03acb40cb..d3a297d43 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -42,6 +42,12 @@ in profiler.HExtlib.profile foo () (CicUnification.UnificationFailure msg) -> raise (RefineFailure msg) | (CicUnification.Uncertain msg) -> raise (Uncertain msg) ;; + +let enrich f = + function + RefineFailure msg -> raise (RefineFailure (f msg)) + | Uncertain msg -> raise (Uncertain (f msg)) + | _ -> assert false let rec split l n = match (l,n) with @@ -152,7 +158,6 @@ let exp_impl metasenv subst context term = in let funs' = combine (funs, types) in metasenv', Cic.CoFix (i, funs') - | term -> metasenv,term and do_subst metasenv context subst = List.fold_right (fun (uri, term) (metasenv, substs) -> @@ -361,14 +366,11 @@ and type_of_aux' metasenv context t ugraph = let te',inferredty,subst'',metasenv'',ugraph2 = type_of_aux subst' metasenv' context te ugraph1 in - (try let subst''',metasenv''',ugraph3 = fo_unif_subst subst'' context metasenv'' - inferredty ty ugraph2 + inferredty ty' ugraph2 in C.Cast (te',ty'),ty',subst''',metasenv''',ugraph3 - with - | _ -> raise (RefineFailure (lazy "Cast"))) | C.Prod (name,s,t) -> let carr t subst context = CicMetaSubst.apply_subst subst t in let coerce_to_sort @@ -396,12 +398,13 @@ and type_of_aux' metasenv context t ugraph = let search = CoercGraph.look_for_coercion in let boh = search coercion_src coercion_tgt in (match boh with - | CoercGraph.NoCoercion -> - raise (RefineFailure (lazy "no coercion")) + | CoercGraph.NoCoercion | CoercGraph.NotHandled _ -> - raise (RefineFailure (lazy "not a sort in PI")) + raise + (RefineFailure (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) | CoercGraph.NotMetaClosed -> - raise (Uncertain (lazy "Coercions on metas 1")) + raise + (Uncertain (lazy (CicMetaSubst.ppterm subst coercion_src ^ " is not a sort and cannoted be coerced to a sort"))) | CoercGraph.SomeCoercion c -> Cic.Appl [c;t],Cic.Sort tgt_sort,subst, metasenv, ugraph) in @@ -430,22 +433,28 @@ and type_of_aux' metasenv context t ugraph = | C.Lambda (n,s,t) -> let s',sort1,subst',metasenv',ugraph1 = - type_of_aux subst metasenv context s ugraph - in - (match CicReduction.whd ~subst:subst' context sort1 with + type_of_aux subst metasenv context s ugraph in + let s',sort1 = + match CicReduction.whd ~subst:subst' context sort1 with C.Meta _ - | C.Sort _ -> () - | _ -> - raise (RefineFailure (lazy (sprintf - "Not well-typed lambda-abstraction: the source %s should be a type; - instead it is a term of type %s" (CicPp.ppterm s) - (CicPp.ppterm sort1)))) - ) ; + | C.Sort _ -> s',sort1 + | 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 + match boh with + | CoercGraph.SomeCoercion c -> + Cic.Appl [c;s'], coercion_tgt + | CoercGraph.NoCoercion + | CoercGraph.NotHandled _ + | CoercGraph.NotMetaClosed -> + raise (RefineFailure (lazy (sprintf + "Not well-typed lambda-abstraction: the source %s should be a type; instead it is a term of type %s" (CicPp.ppterm s) (CicPp.ppterm sort1)))) + in let context_for_t = ((Some (n,(C.Decl s')))::context) in let metasenv',t = exp_impl metasenv' subst' context_for_t t in let t',type2,subst'',metasenv'',ugraph2 = - type_of_aux subst' metasenv' - context_for_t t ugraph1 + type_of_aux subst' metasenv' context_for_t t ugraph1 in C.Lambda (n,s',t'),C.Prod (n,s',type2), subst'',metasenv'',ugraph2 @@ -481,8 +490,16 @@ and type_of_aux' metasenv context t ugraph = ) tl ([],subst',metasenv',ugraph1) in let tl',applty,subst''',metasenv''',ugraph3 = - eat_prods subst'' metasenv'' context + try + eat_prods true subst'' metasenv'' context hetype tlbody_and_type ugraph2 + with + exn -> + enrich + (fun msg -> + lazy ("The application " ^ + CicMetaSubst.ppterm_in_context subst'' t context ^ + " is not well typed:\n" ^ Lazy.force msg)) exn in C.Appl (he'::tl'), applty,subst''',metasenv''',ugraph3 | C.Appl _ -> raise (RefineFailure (lazy "Appl: no arguments")) @@ -744,6 +761,22 @@ and type_of_aux' metasenv context t ugraph = (Cic.Appl (outtype::right_args@[term']))), subst,metasenv,ugraph) | _ -> (* easy case *) + let outtype,outtypety, subst, metasenv,ugraph4 = + type_of_aux subst metasenv context outtype ugraph4 + in + let tlbody_and_type,subst,metasenv,ugraph4 = + List.fold_right + (fun x (res,subst,metasenv,ugraph) -> + let x',ty,subst',metasenv',ugraph1 = + type_of_aux subst metasenv context x ugraph + in + (x', ty)::res,subst',metasenv',ugraph1 + ) (right_args @ [term']) ([],subst,metasenv,ugraph4) + in + let _,_,subst,metasenv,ugraph4 = + eat_prods false subst metasenv context + outtypety tlbody_and_type ugraph4 + in let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context (C.Appl ((outtype :: right_args) @ [term'])) ugraph4 @@ -1001,7 +1034,9 @@ and type_of_aux' metasenv context t ugraph = (CicPp.ppterm t1) (CicPp.ppterm t1'') (CicPp.ppterm t2) (CicPp.ppterm t2'')))) - and eat_prods subst metasenv context hetype tlbody_and_type ugraph = + and eat_prods + allow_coercions subst metasenv context hetype tlbody_and_type ugraph + = let rec mk_prod metasenv context = function [] -> @@ -1068,7 +1103,7 @@ and type_of_aux' metasenv context t ugraph = fo_unif_subst subst context metasenv hety s ugraph in hete,subst,metasenv,ugraph1 - with exn -> + with exn when allow_coercions -> (* we search a coercion from hety to s *) let coer = let carr t subst context = @@ -1080,7 +1115,17 @@ and type_of_aux' metasenv context t ugraph = in match coer with | CoercGraph.NoCoercion - | CoercGraph.NotHandled _ -> raise exn + | CoercGraph.NotHandled _ -> + let msg e = + lazy ("The term " ^ + CicMetaSubst.ppterm_in_context subst hete + context ^ " has type " ^ + CicMetaSubst.ppterm_in_context subst hety + context ^ " but is here used with type " ^ + CicMetaSubst.ppterm_in_context subst s context + (* "\nReason: " ^ Lazy.force e*)) + in + enrich msg exn | CoercGraph.NotMetaClosed -> raise (Uncertain (lazy "Coercions on meta")) | CoercGraph.SomeCoercion c -> @@ -1088,8 +1133,7 @@ and type_of_aux' metasenv context t ugraph = in let coerced_args,metasenv',subst',t',ugraph2 = eat_prods metasenv subst context - (* (CicMetaSubst.subst subst hete t) tl *) - (CicSubstitution.subst hete t) ugraph1 tl + (CicSubstitution.subst arg t) ugraph1 tl in arg::coerced_args,metasenv',subst',t',ugraph2 | _ -> assert false