From c8c7bcfd5fd3086be09c2f949b90c614596489b2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 8 Jun 2005 15:17:15 +0000 Subject: [PATCH] Yet another bug fixed in the inference of the outtype for match: convertibility was used in place of unification, making type inference much less powerful in several useful cases. --- helm/ocaml/cic_unification/cicRefine.ml | 38 +++++++++++++++++-------- 1 file changed, 26 insertions(+), 12 deletions(-) diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml index 8828a417e..25af88f4f 100644 --- a/helm/ocaml/cic_unification/cicRefine.ml +++ b/helm/ocaml/cic_unification/cicRefine.ml @@ -434,7 +434,7 @@ and type_of_aux' metasenv context t ugraph = (match outtype with | C.Meta (n,l) -> - (let candidate,ugraph5,metasenv = + (let candidate,ugraph5,metasenv,subst = let exp_name_subst, metasenv = let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri @@ -503,19 +503,19 @@ and type_of_aux' metasenv context t ugraph = add_lambdas (Cic.Meta (new_meta,irl)) arity_instantiated_with_left_args in - (Some candidate),ugraph4,metasenv + (Some candidate),ugraph4,metasenv,subst | (constructor_args_no,_,instance,_)::tl -> try let instance' = CicSubstitution.delift constructor_args_no (CicMetaSubst.apply_subst subst instance) in - let candidate,ugraph,metasenv = + let candidate,ugraph,metasenv,subst = List.fold_left ( - fun (candidate_oty,ugraph,metasenv) + fun (candidate_oty,ugraph,metasenv,subst) (constructor_args_no,_,instance,_) -> match candidate_oty with - | None -> None,ugraph,metasenv + | None -> None,ugraph,metasenv,subst | Some ty -> try let instance' = @@ -523,6 +523,14 @@ and type_of_aux' metasenv context t ugraph = constructor_args_no (CicMetaSubst.apply_subst subst instance) in +prerr_endline ("PRIMA subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst); + let subst,metasenv,ugraph = + fo_unif_subst subst context metasenv + instance' ty ugraph + in +prerr_endline ("DOPO subst:\n" ^ CicMetaSubst.ppsubst subst ^ "\nmetasenv:\n" ^ CicMetaSubst.ppmetasenv metasenv subst); + candidate_oty,ugraph,metasenv,subst +(* CSC: XXX let b,ugraph1 = CicReduction.are_convertible context instance' ty ugraph @@ -531,11 +539,16 @@ and type_of_aux' metasenv context t ugraph = candidate_oty,ugraph1,metasenv else None,ugraph,metasenv - with Failure s -> None,ugraph,metasenv - ) (Some instance',ugraph4,metasenv) tl +*) + with + Failure _ + | CicUnification.UnificationFailure _ + | CicUnification.Uncertain _ -> + None,ugraph,metasenv,subst + ) (Some instance',ugraph4,metasenv,subst) tl in match candidate with - | None -> None, ugraph,metasenv + | None -> None, ugraph,metasenv,subst | Some t -> let rec add_lambdas n b = function @@ -547,19 +560,20 @@ and type_of_aux' metasenv context t ugraph = in Some (add_lambdas 0 t arity_instantiated_with_left_args), - ugraph,metasenv + ugraph,metasenv,subst with Failure s -> - None,ugraph4,metasenv + None,ugraph4,metasenv,subst in match candidate with | None -> raise (Uncertain "can't solve an higher order unification problem") | Some candidate -> - let s,m,u = + let subst,metasenv,ugraph = fo_unif_subst subst context metasenv candidate outtype ugraph5 in C.MutCase (uri, i, outtype, term', pl'), - (Cic.Appl (outtype::right_args@[term'])),s,m,u) + (Cic.Appl (outtype::right_args@[term'])), + subst,metasenv,ugraph) | _ -> (* easy case *) let _,_, subst, metasenv,ugraph5 = type_of_aux subst metasenv context -- 2.39.2