diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/clenv.ml | 15 | ||||
| -rw-r--r-- | pretyping/evd.ml | 18 | ||||
| -rw-r--r-- | pretyping/termops.ml | 5 | ||||
| -rw-r--r-- | pretyping/termops.mli | 3 |
4 files changed, 37 insertions, 4 deletions
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 074dd0901a..c91580044a 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -222,13 +222,24 @@ let dependent_metas clenv mvs conclmetas = Metaset.union deps (clenv_metavars clenv.evd mv)) mvs conclmetas +let duplicated_metas c = + let rec collrec (one,more as acc) c = + match kind_of_term c with + | Meta mv -> if List.mem mv one then (one,mv::more) else (mv::one,more) + | _ -> fold_constr collrec acc c + in + snd (collrec ([],[]) c) + let clenv_dependent hyps_only clenv = let mvs = undefined_metas clenv.evd in let ctyp_mvs = (mk_freelisted (clenv_type clenv)).freemetas in let deps = dependent_metas clenv mvs ctyp_mvs in + let nonlinear = duplicated_metas (clenv_value clenv) in + (* Make the assumption that duplicated metas have internal dependencies *) List.filter - (fun mv -> Metaset.mem mv deps && - not (hyps_only && Metaset.mem mv ctyp_mvs)) + (fun mv -> (Metaset.mem mv deps && + not (hyps_only && Metaset.mem mv ctyp_mvs)) + or List.mem mv nonlinear) mvs let clenv_missing ce = clenv_dependent true ce diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 660547b5ce..166114ab63 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -643,6 +643,20 @@ type unsolvability_explanation = SeveralInstancesFound of int (**********************************************************) (* Pretty-printing *) +let pr_instance_status (sc,typ) = + begin match sc with + | IsSubType -> str " [or a subtype of it]" + | IsSuperType -> str " [or a supertype of it]" + | ConvUpToEta 0 -> mt () + | UserGiven -> mt () + | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]" + end ++ + begin match typ with + | CoerceToType -> str " [up to coercion]" + | TypeNotProcessed -> mt () + | TypeProcessed -> str " [type is checked]" + end + let pr_meta_map mmap = let pr_name = function Name id -> str"[" ++ pr_id id ++ str"]" @@ -652,10 +666,10 @@ let pr_meta_map mmap = hov 0 (pr_meta mv ++ pr_name na ++ str " : " ++ print_constr b.rebus ++ fnl ()) - | (mv,Clval(na,(b,_),_)) -> + | (mv,Clval(na,(b,s),_)) -> hov 0 (pr_meta mv ++ pr_name na ++ str " := " ++ - print_constr b.rebus ++ fnl ()) + print_constr b.rebus ++ spc () ++ pr_instance_status s ++ fnl ()) in prlist pr_meta_binding (metamap_to_list mmap) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 73c03097af..4246f0daa5 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with | Cast (c,_,_) -> strip_head_cast c | _ -> c +(* Get the last arg of an application *) +let last_arg c = match kind_of_term c with + | App (f,cl) -> array_last cl + | _ -> anomaly "last_arg" + (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name list) which is processed by [g na] (which typically cons [na] to diff --git a/pretyping/termops.mli b/pretyping/termops.mli index f80deab10c..539951d5c4 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -185,6 +185,9 @@ val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr val it_mkProd_or_LetIn_name : env -> types -> rel_context -> types val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr +(* Get the last arg of a constr intended to be nn application *) +val last_arg : constr -> constr + (* name contexts *) type names_context = name list val add_name : name -> names_context -> names_context |