X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=130799ea432a7ee1426d7645099c0c40e6a4c5d4;hb=de9a83f286eee12117fb478ea2db18f7faebac9a;hp=cebbb9e8f68d2bc1fadc45f2fbca438fad2bf617;hpb=cf5d6fab96c47ccb7d623d72742717d9b08bae7b;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index cebbb9e8f..130799ea4 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -31,9 +31,9 @@ exception AssertFailure of string;; let debug_print = prerr_endline -let type_of_aux' metasenv subst context term = +let type_of_aux' metasenv subst context term ugraph = try - CicTypeChecker.type_of_aux' ~subst metasenv context term + CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph with CicTypeChecker.TypeCheckerFailure msg -> let msg = @@ -47,8 +47,9 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppsubst subst) msg) in raise (AssertFailure msg);; (* +>>>>>>> 1.40 try - CicMetaSubst.type_of_aux' metasenv subst context term + CicMetaSubst.type_of_aux' metasenv subst context term ugraph with | CicMetaSubst.MetaSubstFailure msg -> raise (AssertFailure @@ -59,37 +60,56 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppmetasenv metasenv subst) msg))) *) let rec deref subst = + let snd (_,a,_) = a in function Cic.Meta(n,l) as t -> (try deref subst - (CicSubstitution.lift_meta + (CicSubstitution.subst_meta l (snd (CicUtil.lookup_subst n subst))) with CicUtil.Subst_not_found _ -> t) | t -> t ;; -let rec beta_expand test_equality_only metasenv subst context t arg = +let rec beta_expand test_equality_only metasenv subst context t arg ugraph = let module S = CicSubstitution in let module C = Cic in - let rec aux metasenv subst n context t' = + let rec aux metasenv subst n context t' ugraph = try - let subst,metasenv = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n arg) t' + + let subst,metasenv,ugraph1 = + fo_unif_subst test_equality_only subst context metasenv + (CicSubstitution.lift n arg) t' ugraph + in - subst,metasenv,C.Rel (1 + n) + subst,metasenv,C.Rel (1 + n),ugraph1 with Uncertain _ | UnificationFailure _ -> match t' with - | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1) + | C.Rel m -> subst,metasenv, + (if m <= n then C.Rel m else C.Rel (m+1)),ugraph | C.Var (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst' = - aux_exp_named_subst metasenv subst n context exp_named_subst + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph in - subst,metasenv,C.Var (uri,exp_named_subst') +(* THIS WAS BEFORE ---- + subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 + | C.Meta (i,l) as t-> + (try + let (_, t') = CicMetaSubst.lookup_subst i subst in + aux metasenv subst n context (CicSubstitution.subst_meta l t') + ugraph + with CicMetaSubst.SubstNotFound _ -> + let (subst, metasenv, context, local_context,ugraph1) = + List.fold_left + (fun (subst, metasenv, context, local_context,ugraph) t -> + match t with + | None -> + (subst, metasenv, context, None::local_context, ugraph) +--------- *) + subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 | C.Meta (i,l) -> (* andrea: in general, beta_expand can create badly typed terms. This happens quite seldom in practice, UNLESS we @@ -100,81 +120,105 @@ let rec beta_expand test_equality_only metasenv subst context t arg = (function Some t -> Some (CicSubstitution.lift 1 t) | None -> None) l in - subst, metasenv, C.Meta (i,l) + subst, metasenv, C.Meta (i,l), ugraph (* let (subst, metasenv, context, local_context) = List.fold_right (fun t (subst, metasenv, context, local_context) -> match t with | None -> (subst, metasenv, context, None :: local_context) + | Some t -> - let (subst, metasenv, t) = - aux metasenv subst n context t + let (subst, metasenv, t, ugraph1) = + aux metasenv subst n context t ugraph in +(* THIS WAS BEFORE ---- + (subst, metasenv, context, + (Some t)::local_context,ugraph1)) + (subst, metasenv, context, [],ugraph) l + in + (subst, metasenv,(C.Meta (i, local_context)),ugraph1)) +-------- *) (subst, metasenv, context, Some t :: local_context)) l (subst, metasenv, context, []) in prerr_endline ("nuova meta :" ^ (CicPp.ppterm (C.Meta (i, local_context)))); (subst, metasenv, C.Meta (i, local_context)) *) | C.Sort _ - | C.Implicit _ as t -> subst,metasenv,t + | C.Implicit _ as t -> subst,metasenv,t,ugraph | C.Cast (te,ty) -> - let subst,metasenv,te' = aux metasenv subst n context te in - let subst,metasenv,ty' = aux metasenv subst n context ty in - subst,metasenv,C.Cast (te', ty') + let subst,metasenv,te',ugraph1 = + aux metasenv subst n context te ugraph in + let subst,metasenv,ty',ugraph2 = + aux metasenv subst n context ty ugraph1 in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Cast (te', ty')),ugraph2 | C.Prod (nn,s,t) -> - let subst,metasenv,s' = aux metasenv subst n context s in - let subst,metasenv,t' = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + ugraph1 in - subst,metasenv,C.Prod (nn, s', t') + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Prod (nn, s', t')),ugraph2 | C.Lambda (nn,s,t) -> - let subst,metasenv,s' = aux metasenv subst n context s in - let subst,metasenv,t' = - aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 in - subst,metasenv,C.Lambda (nn, s', t') + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 | C.LetIn (nn,s,t) -> - let subst,metasenv,s' = aux metasenv subst n context s in - let subst,metasenv,t' = + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t + ugraph1 in - subst,metasenv,C.LetIn (nn, s', t') + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.LetIn (nn, s', t')),ugraph2 | C.Appl l -> - let subst,metasenv,revl' = + let subst,metasenv,revl',ugraph1 = List.fold_left - (fun (subst,metasenv,appl) t -> - let subst,metasenv,t' = aux metasenv subst n context t in - subst,metasenv,t'::appl - ) (subst,metasenv,[]) l + (fun (subst,metasenv,appl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::appl),ugraph1 + ) (subst,metasenv,[],ugraph) l in - subst,metasenv,C.Appl (List.rev revl') + subst,metasenv,(C.Appl (List.rev revl')),ugraph1 | C.Const (uri,exp_named_subst) -> - let subst,metasenv,exp_named_subst' = - aux_exp_named_subst metasenv subst n context exp_named_subst + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph in - subst,metasenv,C.Const (uri,exp_named_subst') + subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 | C.MutInd (uri,i,exp_named_subst) -> - let subst,metasenv,exp_named_subst' = - aux_exp_named_subst metasenv subst n context exp_named_subst + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph in - subst,metasenv,C.MutInd (uri,i,exp_named_subst') + subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 | C.MutConstruct (uri,i,j,exp_named_subst) -> - let subst,metasenv,exp_named_subst' = - aux_exp_named_subst metasenv subst n context exp_named_subst + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph in - subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst') + subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 | C.MutCase (sp,i,outt,t,pl) -> - let subst,metasenv,outt' = aux metasenv subst n context outt in - let subst,metasenv,t' = aux metasenv subst n context t in - let subst,metasenv,revpl' = + let subst,metasenv,outt',ugraph1 = + aux metasenv subst n context outt ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst n context t ugraph1 in + let subst,metasenv,revpl',ugraph3 = List.fold_left - (fun (subst,metasenv,pl) t -> - let subst,metasenv,t' = aux metasenv subst n context t in - subst,metasenv,t'::pl - ) (subst,metasenv,[]) pl + (fun (subst,metasenv,pl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::pl),ugraph1 + ) (subst,metasenv,[],ugraph2) pl in - subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl') + subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 + (* TASSI: not sure this is serial *) | C.Fix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -184,8 +228,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg = fl in C.Fix (i, substitutedfl) -*) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *) - subst,metasenv,CicSubstitution.lift 1 t' +*) + subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph | C.CoFix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -195,36 +239,49 @@ let rec beta_expand test_equality_only metasenv subst context t arg = fl in C.CoFix (i, substitutedfl) -*) (* subst,metasenv,CicMetasubst.lift subst 1 t' *) - subst,metasenv,CicSubstitution.lift 1 t' - and aux_exp_named_subst metasenv subst n context ens = +*) + subst,metasenv,(CicSubstitution.lift 1 t'), ugraph + + and aux_exp_named_subst metasenv subst n context ens ugraph = List.fold_right - (fun (uri,t) (subst,metasenv,l) -> - let subst,metasenv,t' = aux metasenv subst n context t in - subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) + (fun (uri,t) (subst,metasenv,l,ugraph) -> + let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in + subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) in - let argty = type_of_aux' metasenv subst context arg in + let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in let fresh_name = - FreshNamesGenerator.mk_fresh_name + FreshNamesGenerator.mk_fresh_name ~subst metasenv context (Cic.Name "Heta") ~typ:argty in - let subst,metasenv,t' = aux metasenv subst 0 context t in + let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in (* prova *) (* old subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] *) - subst, metasenv, C.Lambda (fresh_name,argty,t') + subst, metasenv, C.Lambda (fresh_name,argty,t'), ugraph2 + -and beta_expand_many test_equality_only metasenv subst context t args = - let subst,metasenv,hd = +(* WAS --------- +and beta_expand_many test_equality_only metasenv subst context t l ugraph = + List.fold_left + (fun (subst,metasenv,t,ugraph) arg -> + beta_expand test_equality_only metasenv subst context t arg ugraph + ) (subst,metasenv,t,ugraph) l +------- *) +and beta_expand_many test_equality_only metasenv subst context t args ugraph = + let subst,metasenv,hd,ugraph = List.fold_right - (fun arg (subst,metasenv,t) -> - let subst,metasenv,t = - beta_expand test_equality_only metasenv subst context t arg in - subst,metasenv,t - ) args (subst,metasenv,t) in - subst,metasenv,hd + (fun arg (subst,metasenv,t,ugraph) -> + let subst,metasenv,t,ugraph1 = + beta_expand test_equality_only + metasenv subst context t arg ugraph + in + subst,metasenv,t,ugraph1 + ) args (subst,metasenv,t,ugraph) + in + subst,metasenv,hd,ugraph + (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -235,44 +292,94 @@ and beta_expand_many test_equality_only metasenv subst context t args = a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -and fo_unif_subst test_equality_only subst context metasenv t1 t2 = +and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph = let module C = Cic in let module R = CicReduction in let module S = CicSubstitution in let t1 = deref subst t1 in let t2 = deref subst t2 in - match (t1, t2) with - (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let _,subst,metasenv = + let b,ugraph = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph + in + if b then + subst, metasenv, ugraph + else + match (t1, t2) with + (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> +(* + let ok,subst,metasenv,ugraph1 = + try + List.fold_left2 + (fun (b,subst,metasenv,ugraph) t1 t2 -> + if b then true,subst,metasenv,ugraph else + match t1,t2 with + None,_ + | _,None -> true,subst,metasenv,ugraph + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + let b',ugraph1 = + R.are_convertible subst context t1' t2' ugraph in + if b' then + true,subst,metasenv,ugraph1 + else + (try + let subst,metasenv,ugraph2 = + fo_unif_subst + (* TASSI: is this another try that should use ugraph? *) + test_equality_only subst context metasenv t1' t2' ugraph + in + true,subst,metasenv,ugraph2 + with + Not_found -> false,subst,metasenv,ugraph1) + ) (true,subst,metasenv,ugraph) ln lm + with + Invalid_argument _ -> + raise (UnificationFailure (sprintf + "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + in + if ok then + subst,metasenv,ugraph1 + else + raise (UnificationFailure (sprintf + "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted." + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + *) + let _,subst,metasenv,ugraph1 = (try List.fold_left2 - (fun (j,subst,metasenv) t1 t2 -> + (fun (j,subst,metasenv,ugraph) t1 t2 -> match t1,t2 with None,_ - | _,None -> j+1,subst,metasenv + | _,None -> j+1,subst,metasenv,ugraph | Some t1', Some t2' -> (* First possibility: restriction *) (* Second possibility: unification *) (* Third possibility: convertibility *) - if R.are_convertible ~subst ~metasenv context t1' t2' then - j+1,subst,metasenv - else - (try - let subst,metasenv = - fo_unif_subst - test_equality_only - subst context metasenv t1' t2' - in - j+1,subst,metasenv - with - Uncertain _ - | UnificationFailure _ -> + let b, ugraph1 = + R.are_convertible + ~subst ~metasenv context t1' t2' ugraph + in + if b then + j+1,subst,metasenv, ugraph1 + else + (try + let subst,metasenv,ugraph2 = + fo_unif_subst + test_equality_only + subst context metasenv t1' t2' ugraph + in + j+1,subst,metasenv,ugraph2 + with + Uncertain _ + | UnificationFailure _ -> prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)); let metasenv, subst = CicMetaSubst.restrict subst [(n,j)] metasenv in - j+1,subst,metasenv) - ) (1,subst,metasenv) ln lm + j+1,subst,metasenv,ugraph1) + ) (1,subst,metasenv,ugraph) ln lm with Exit -> raise @@ -287,9 +394,10 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str (* (sprintf "Error trying to unify %s with %s: the lengths of the two local contexts do not match." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))))*) - in subst,metasenv + in subst,metasenv,ugraph1 + | (C.Meta (n,_), C.Meta (m,_)) when n>m -> - fo_unif_subst test_equality_only subst context metasenv t2 t1 + fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph | (C.Meta (n,l), t) | (t, C.Meta (n,l)) -> let swap = @@ -301,18 +409,93 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str let lower = fun x y -> if swap then y else x in let upper = fun x y -> if swap then x else y in let fo_unif_subst_ordered - test_equality_only subst context metasenv m1 m2 = + test_equality_only subst context metasenv m1 m2 ugraph = fo_unif_subst test_equality_only subst context metasenv - (lower m1 m2) (upper m1 m2) + (lower m1 m2) (upper m1 m2) ugraph in +(* + begin + try + let (_, oldt) = CicMetaSubst.lookup_subst n subst in + let lifted_oldt = S.subst_meta l oldt in + let ty_lifted_oldt,ugraph1 = + type_of_aux' metasenv subst context lifted_oldt ugraph + in + let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in + let (subst, metasenv, ugraph3) = + fo_unif_subst_ordered test_equality_only subst context metasenv + tyt ty_lifted_oldt ugraph2 + in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt ugraph3 + with CicMetaSubst.SubstNotFound _ -> + (* First of all we unify the type of the meta with the type of the term *) + let subst,metasenv,ugraph1 = + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in + (try + let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 + with AssertFailure _ -> + (* TODO huge hack!!!! + * we keep on unifying/refining in the hope that the problem will be + * eventually solved. In the meantime we're breaking a big invariant: + * the terms that we are unifying are no longer well typed in the + * current context (in the worst case we could even diverge) + *) +(* +prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN."; +prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; +*) + (subst, metasenv,ugraph)) + in + let t',metasenv,subst = + try + (* TASSI: I hope delift does nothing with universes *) + CicMetaSubst.delift n subst context metasenv l t + with + (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg) + | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) + in + let t'',ugraph2 = + match t' with + C.Sort (C.Type u) when not test_equality_only -> + let u' = CicUniv.fresh () in + let s = C.Sort (C.Type u') in + let ugraph2 = + CicUniv.add_ge (upper u u') (lower u u') ugraph1 in + s,ugraph2 + | _ -> t',ugraph1 + in + (* Unifying the types may have already instantiated n. Let's check *) + try + let (_, oldt) = CicMetaSubst.lookup_subst n subst in + let lifted_oldt = S.subst_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt ugraph2 + with + CicMetaSubst.SubstNotFound _ -> + let (_, context, _) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'')) :: subst in + let metasenv = +(* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *) + CicMetaSubst.apply_subst_metasenv subst metasenv + in + subst, metasenv,ugraph2 +(* (n,t'')::subst, metasenv *) + end +*) begin - let subst,metasenv = + let subst,metasenv,ugraph1 = let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in (try - let tyt = type_of_aux' metasenv subst context t in + let tyt,ugraph1 = + type_of_aux' metasenv subst context t ugraph + in fo_unif_subst test_equality_only - subst context metasenv tyt (S.lift_meta l meta_type) + subst context metasenv tyt (S.subst_meta l meta_type) ugraph1 with UnificationFailure msg | Uncertain msg -> @@ -326,7 +509,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str * the terms that we are unifying are no longer well * typed in the current context (in the worst case * we could even diverge) *) - (subst, metasenv)) in + (subst, metasenv,ugraph)) in let t',metasenv,subst = try CicMetaSubst.delift n subst context metasenv l t @@ -335,34 +518,37 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str raise (UnificationFailure msg) | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg) in - let t'' = + let t'',ugraph2 = match t' with C.Sort (C.Type u) when not test_equality_only -> let u' = CicUniv.fresh () in let s = C.Sort (C.Type u') in - ignore (CicUniv.add_ge (upper u u') (lower u u')) ; - s - | _ -> t' + let ugraph2 = + CicUniv.add_ge (upper u u') (lower u u') ugraph1 + in + s,ugraph2 + | _ -> t',ugraph1 in (* Unifying the types may have already instantiated n. Let's check *) try - let (_, oldt) = CicUtil.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in + let (_, oldt,_) = CicUtil.lookup_subst n subst in + let lifted_oldt = S.subst_meta l oldt in fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt + test_equality_only subst context metasenv t lifted_oldt ugraph2 with CicUtil.Subst_not_found _ -> - let (_, context, _) = CicUtil.lookup_meta n metasenv in - let subst = (n, (context, t'')) :: subst in + let (_, context, ty) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'',ty)) :: subst in let metasenv = List.filter (fun (m,_,_) -> not (n = m)) metasenv in - subst, metasenv + subst, metasenv, ugraph2 end + | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2)) | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) -> if UriManager.eq uri1 uri2 then fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 + exp_named_subst1 exp_named_subst2 ugraph else raise (UnificationFailure "3") (* (sprintf @@ -371,7 +557,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 then fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 + exp_named_subst1 exp_named_subst2 ugraph else raise (UnificationFailure "4") (* (sprintf @@ -381,7 +567,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str C.MutConstruct (uri2,i2,j2,exp_named_subst2) -> if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 + exp_named_subst1 exp_named_subst2 ugraph else raise (UnificationFailure "5") (* (sprintf @@ -389,26 +575,36 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only - subst context metasenv te t2 + subst context metasenv te t2 ugraph | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only - subst context metasenv t1 te + subst context metasenv t1 te ugraph | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - (* TASSI: this is the only case in which we want == *) - let subst',metasenv' = fo_unif_subst true - subst context metasenv s1 s2 in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + let subst',metasenv',ugraph1 = + fo_unif_subst true subst context metasenv s1 s2 ugraph + in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - (* TASSI: ask someone a reason for not putting true here *) - let subst',metasenv' = fo_unif_subst test_equality_only - subst context metasenv s1 s2 in - fo_unif_subst test_equality_only - subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + let subst',metasenv',ugraph1 = + fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph + in + fo_unif_subst test_equality_only + subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 ugraph1 | (C.LetIn (_,s1,t1), t2) | (t2, C.LetIn (_,s1,t1)) -> fo_unif_subst - test_equality_only subst context metasenv t2 (S.subst s1 t1) + test_equality_only subst context metasenv t2 (S.subst s1 t1) ugraph | (C.Appl l1, C.Appl l2) -> +(* WAS BEFORE ---------- + let subst,metasenv,t1',t2',ugraph1 = + match l1,l2 with + C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j -> + subst,metasenv,t1,t2,ugraph + (* In the first two cases when we reach the next begin ... end + section useless work is done since, by construction, the list + of arguments will be equal. + *) +----------------- *) (* andrea: this case should be probably rewritten in the spirit of deref *) let rec beta_reduce = @@ -420,72 +616,98 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str else beta_reduce (Cic.Appl(he''::tl')) | t -> t in + let exists_a_meta l = + List.exists (function Cic.Meta _ -> true | _ -> false) l + in (match l1,l2 with C.Meta (i,_)::args1, C.Meta (j,_)::args2 when i = j -> (try List.fold_left2 - (fun (subst,metasenv) -> - fo_unif_subst test_equality_only subst context metasenv) - (subst,metasenv) l1 l2 + (fun (subst,metasenv,ugraph) t1 t2 -> + fo_unif_subst + test_equality_only subst context metasenv t1 t2 ugraph) + (subst,metasenv,ugraph) l1 l2 with (Invalid_argument msg) -> raise (UnificationFailure msg)) - | C.Meta (i,l)::args, _ -> + | C.Meta (i,l)::args, _ when not(exists_a_meta args) -> + (* we verify that none of the args is a Meta, since beta expanding + with respoect to a metavariable makes no sense + *) (try - let (_,t) = CicUtil.lookup_subst i subst in - let lifted = S.lift_meta l t in + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only - subst context metasenv reduced t2 + subst context metasenv reduced t2 ugraph with CicUtil.Subst_not_found _ -> - let subst,metasenv,beta_expanded = + let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many - test_equality_only metasenv subst context t2 args in - fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded) - | _, C.Meta (i,l)::args -> + test_equality_only metasenv subst context t2 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1) + | _, C.Meta (i,l)::args when not(exists_a_meta args) -> (try - let (_,t) = CicUtil.lookup_subst i subst in - let lifted = S.lift_meta l t in + let (_,t,_) = CicUtil.lookup_subst i subst in + let lifted = S.subst_meta l t in let reduced = beta_reduce (Cic.Appl (lifted::args)) in fo_unif_subst test_equality_only - subst context metasenv t1 reduced + subst context metasenv t1 reduced ugraph with CicUtil.Subst_not_found _ -> - let subst,metasenv,beta_expanded = + let subst,metasenv,beta_expanded,ugraph1 = beta_expand_many - test_equality_only metasenv subst context t1 args in + test_equality_only metasenv subst context t1 args ugraph in fo_unif_subst test_equality_only subst context metasenv - (C.Meta (i,l)) beta_expanded) + (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 fo_unif_l test_equality_only subst metasenv = - function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_subst test_equality_only subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> + let rec + fo_unif_l test_equality_only subst metasenv (l1,l2) ugraph = + match (l1,l2) with + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_subst + test_equality_only subst context metasenv h1 h2 ugraph + | ([h],l) + | (l,[h]) -> fo_unif_subst test_equality_only subst context metasenv - h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_subst test_equality_only subst context metasenv h1 h2 + h (C.Appl (List.rev l)) ugraph + | ((h1::l1),(h2::l2)) -> + let subst', metasenv',ugraph1 = + fo_unif_subst + test_equality_only subst context metasenv h1 h2 ugraph in - fo_unif_l test_equality_only subst' metasenv' (l1,l2) + fo_unif_l + test_equality_only subst' metasenv' (l1,l2) ugraph1 in - fo_unif_l test_equality_only subst metasenv (lr1, lr2) ) + fo_unif_l + test_equality_only subst metasenv (lr1, lr2) ugraph)(**) | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> - let subst', metasenv' = - fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in - let subst'',metasenv'' = - fo_unif_subst test_equality_only subst' context metasenv' t1' t2' in + let subst', metasenv',ugraph1 = + fo_unif_subst test_equality_only subst context metasenv outt1 outt2 + ugraph in + let subst'',metasenv'',ugraph2 = + fo_unif_subst test_equality_only subst' context metasenv' t1' t2' + ugraph1 in (try List.fold_left2 - (function (subst,metasenv) -> - fo_unif_subst test_equality_only subst context metasenv - ) (subst'',metasenv'') pl1 pl2 + (fun (subst,metasenv,ugraph) t1 t2 -> + fo_unif_subst + test_equality_only subst context metasenv t1 t2 ugraph + ) (subst'',metasenv'',ugraph2) pl1 pl2 with Invalid_argument _ -> raise (UnificationFailure "6")) @@ -493,7 +715,7 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str "Error trying to unify %s with %s: the number of branches is not the same." (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2)))) *) | (C.Rel _, _) | (_, C.Rel _) -> if t1 = t2 then - subst, metasenv + subst, metasenv,ugraph else raise (UnificationFailure "6") (* (sprintf @@ -505,31 +727,42 @@ prerr_endline ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (str | (C.MutConstruct _, _) | (_, C.MutConstruct _) | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) | (_, C.CoFix _) -> - if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then - subst, metasenv - else - raise (UnificationFailure "7") - (* (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + if t1 = t2 then + subst, metasenv, ugraph + else + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph + in + if b then + subst, metasenv, ugraph1 + else + raise (UnificationFailure "7") + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2))) *) | (_,_) -> - if R.are_convertible ~subst ~metasenv context t1 t2 then - subst, metasenv - else - raise (UnificationFailure "8") - (* (sprintf - "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph + in + if b then + subst, metasenv, ugraph1 + else + raise (UnificationFailure "8") + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) + (CicMetaSubst.ppterm subst t2))) *) and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv - exp_named_subst1 exp_named_subst2 + exp_named_subst1 exp_named_subst2 ugraph = try List.fold_left2 - (fun (subst,metasenv) (uri1,t1) (uri2,t2) -> + (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) -> assert (uri1=uri2) ; - fo_unif_subst test_equality_only subst context metasenv t1 t2 - ) (subst,metasenv) exp_named_subst1 exp_named_subst2 + fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph + ) (subst,metasenv,ugraph) exp_named_subst1 exp_named_subst2 with Invalid_argument _ -> let print_ens ens = @@ -549,26 +782,28 @@ and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv (* a new substitution which is already unwinded and ready to be applied and *) (* a new metasenv in which some hypothesis in the contexts of the *) (* metavariables may have been restricted. *) -let fo_unif metasenv context t1 t2 = - fo_unif_subst false [] context metasenv t1 t2 ;; +let fo_unif metasenv context t1 t2 ugraph = + fo_unif_subst false [] context metasenv t1 t2 ugraph ;; -let fo_unif_subst subst context metasenv t1 t2 = +let fo_unif_subst subst context metasenv t1 t2 ugraph = let enrich_msg msg = (* "bella roba" *) sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nand substitution\n%s\nbecause %s" (CicMetaSubst.ppterm subst t1) (try - CicPp.ppterm (type_of_aux' metasenv subst context t1) + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicPp.ppterm ty_t1 with _ -> "MALFORMED") (CicMetaSubst.ppterm subst t2) (try - CicPp.ppterm (type_of_aux' metasenv subst context t2) + let ty_t2,_ = type_of_aux' metasenv subst context t2 ugraph in + CicPp.ppterm ty_t2 with _ -> "MALFORMED") (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv metasenv subst) (CicMetaSubst.ppsubst subst) msg in try - fo_unif_subst false subst context metasenv t1 t2 + fo_unif_subst false subst context metasenv t1 t2 ugraph with | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg))