From d1d5e134c680aaa1cab15a35b944ca0a3a39c704 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 20 May 2005 15:26:55 +0000 Subject: [PATCH] When we unify a Prod against a term t2 which is not a Prod we now try a whd of t2. --- helm/ocaml/cic_unification/cicUnification.ml | 38 ++++++++------------ 1 file changed, 15 insertions(+), 23 deletions(-) diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 130799ea4..1d6044211 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -46,18 +46,6 @@ let type_of_aux' metasenv subst context term ugraph = (CicMetaSubst.ppmetasenv metasenv subst) (CicMetaSubst.ppsubst subst) msg) in raise (AssertFailure msg);; -(* ->>>>>>> 1.40 - try - CicMetaSubst.type_of_aux' metasenv subst context term ugraph - with - | CicMetaSubst.MetaSubstFailure msg -> - raise (AssertFailure - ((sprintf - "Type checking error: %s in context\n%s\nand metasenv\n%s.\nException: %s.\nBroken invariant: unification must be invoked only on well typed terms" - (CicMetaSubst.ppterm subst term) - (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) msg))) *) let rec deref subst = let snd (_,a,_) = a in @@ -661,16 +649,6 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv (C.Meta (i,l)) beta_expanded ugraph1) | _,_ -> -(* WAS BEFORE ----- -<<<<<<< cicUnification.ml - subst,metasenv,t1,t2,ugraph - in - begin - match t1',t2' with - C.Appl l1, C.Appl l2 -> - let lr1 = List.rev l1 in -======= ---------*) let lr1 = List.rev l1 in let lr2 = List.rev l2 in let rec @@ -741,6 +719,20 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + | (C.Prod _, t2) -> + let t2' = R.whd ~subst context t2 in + (match t2' with + C.Prod _ -> + fo_unif_subst test_equality_only + subst context metasenv t1 t2' ugraph + | _ -> raise (UnificationFailure "8")) + | (t1, C.Prod _) -> + let t1' = R.whd ~subst context t1 in + (match t1' with + C.Prod _ -> + fo_unif_subst test_equality_only + subst context metasenv t1' t2 ugraph + | _ -> raise (UnificationFailure "9")) | (_,_) -> let b,ugraph1 = R.are_convertible ~subst ~metasenv context t1 t2 ugraph @@ -748,7 +740,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; if b then subst, metasenv, ugraph1 else - raise (UnificationFailure "8") + raise (UnificationFailure "10") (* (sprintf "Can't unify %s with %s because they are not convertible" (CicMetaSubst.ppterm subst t1) -- 2.39.2