X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=e521c6570b8958b092bc86a7020b16a3cad0dc20;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=2f27bea85adac6a996c5152d40d5b7635996d1c0;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 2f27bea85..e521c6570 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -23,478 +23,757 @@ * http://cs.unibo.it/helm/. *) -exception UnificationFailed;; -exception Free;; -exception OccurCheck;; -exception RelToHiddenHypothesis;; -exception OpenTerm;; +open Printf -type substitution = (int * Cic.term) list +exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; -(* NUOVA UNIFICAZIONE *) -(* A substitution is a (int * Cic.term) list that associates a - metavariable i with its body. - A metaenv is a (int * Cic.term) list that associate a metavariable - i with is type. - fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back - a new substitution which is _NOT_ unwinded. It must be unwinded before - applying it. *) - -let fo_unif_new metasenv context t1 t2 = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let rec fo_unif_aux subst context metasenv t1 t2 = - match (t1, t2) with - (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> - let ok = - List.fold_left2 - (fun b t1 t2 -> - b && - match t1,t2 with - None,_ - | _,None -> true - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - R.are_convertible context t1' t2' - ) true ln lm +let debug_print = prerr_endline + +let type_of_aux' metasenv subst context term ugraph = + try + CicTypeChecker.type_of_aux' ~subst metasenv context term ugraph + with + CicTypeChecker.TypeCheckerFailure msg -> + let msg = + (sprintf + "Kernel Type checking error: +%s\n%s\ncontext=\n%s\nmetasenv=\n%s\nsubstitution=\n%s\nException:\n%s.\nToo bad." + (CicMetaSubst.ppterm subst term) + (CicMetaSubst.ppterm [] term) + (CicMetaSubst.ppcontext subst context) + (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 + function + Cic.Meta(n,l) as t -> + (try + deref subst + (CicSubstitution.lift_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 ugraph = + let module S = CicSubstitution in + let module C = Cic in + let rec aux metasenv subst n context t' ugraph = + try + + 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),ugraph1 + with + Uncertain _ + | UnificationFailure _ -> + match t' with + | 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',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph in - if ok then subst,metasenv else - raise UnificationFailed - | (C.Meta (n,l), C.Meta (m,_)) when n>m -> - fo_unif_aux subst context metasenv t2 t1 - | (C.Meta (n,l), t) - | (t, C.Meta (n,l)) -> - let subst',metasenv' = - try - let oldt = (List.assoc n subst) in - let lifted_oldt = S.lift_meta l oldt in - fo_unif_aux subst context metasenv lifted_oldt t - with Not_found -> -prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ; -List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; -prerr_endline " m=n) metasenv' in - let tyt = CicTypeChecker.type_of_aux' metasenv' context t in - fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt - | (C.Rel _, _) - | (_, C.Rel _) - | (C.Var _, _) - | (_, C.Var _) - | (C.Sort _ ,_) - | (_, C.Sort _) - | (C.Implicit, _) - | (_, C.Implicit) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in - fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in - fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_aux subst context metasenv t2 (S.subst s1 t1) - | (C.Appl l1, C.Appl l2) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_l subst metasenv = function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_aux subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> - fo_unif_aux subst context metasenv h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_aux subst context metasenv h1 h2 - in - fo_unif_l subst' metasenv' (l1,l2) +(* 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.lift_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 + iterate on the local context. For this reason, we renounce + to iterate and just lift *) + let l = + List.map + (function + Some t -> Some (CicSubstitution.lift 1 t) + | None -> None) l in + 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, 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,ugraph + | 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',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 - fo_unif_l subst metasenv (lr1, lr2) - | (C.Const _, _) - | (_, C.Const _) - | (C.Abst _, _) - | (_, C.Abst _) - | (C.MutInd _, _) - | (_, C.MutInd _) - | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> - let subst', metasenv' = - fo_unif_aux subst context metasenv outt1 outt2 in - let subst'',metasenv'' = - fo_unif_aux subst' context metasenv' t1 t2 in - List.fold_left2 - (function (subst,metasenv) -> - fo_unif_aux subst context metasenv - ) (subst'',metasenv'') pl1 pl2 - | (C.Fix _, _) - | (_, C.Fix _) - | (C.CoFix _, _) - | (_, C.CoFix _) -> - if R.are_convertible context t1 t2 then subst, metasenv - else raise UnificationFailed - | (_,_) -> raise UnificationFailed - in fo_unif_aux [] context metasenv t1 t2;; + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Prod (nn, s', t')),ugraph2 + | C.Lambda (nn,s,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 + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 + | C.LetIn (nn,s,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 + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.LetIn (nn, s', t')),ugraph2 + | C.Appl l -> + let subst,metasenv,revl',ugraph1 = + List.fold_left + (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')),ugraph1 + | C.Const (uri,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')),ugraph1 + | C.MutInd (uri,i,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')),ugraph1 + | C.MutConstruct (uri,i,j,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')),ugraph1 + | C.MutCase (sp,i,outt,t,pl) -> + 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,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')),ugraph3 + (* TASSI: not sure this is serial *) + | C.Fix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo)) + fl + in + C.Fix (i, substitutedfl) +*) + subst,metasenv,(CicSubstitution.lift 1 t' ),ugraph + | C.CoFix (i,fl) -> +(*CSC: not implemented + let tylen = List.length fl in + let substitutedfl = + List.map + (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo)) + fl + in + C.CoFix (i, substitutedfl) -(*CSC: ??????????????? -(* m is the index of a metavariable to restrict, k is nesting depth -of the occurrence m, and l is its relocation list. canonical_context -is the context of the metavariable we are instantiating - containing -m - Only rel in the domain of canonical_context are accessible. -This function takes in input a metasenv and gives back a metasenv. -A rel(j) in the canonical context of m, is rel(List.nth l j) for the -instance of m under consideration, that is rel (List.nth l j) - k -in canonical_context. *) +*) + subst,metasenv,(CicSubstitution.lift 1 t'), ugraph -let restrict canonical_context m k l = - let rec erase i = - function - [] -> [] - | None::tl -> None::(erase (i+1) tl) - | he::tl -> - let i' = (List.nth l (i-1)) in - if i' <= k - then he::(erase (i+1) tl) (* local variable *) - else - let acc = - (try List.nth canonical_context (i'-k-1) - with Failure _ -> None) in - if acc = None - then None::(erase (i+1) tl) - else he::(erase (i+1) tl) in - let rec aux = - function - [] -> [] - | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl - | hd::tl -> hd::(aux tl) + and aux_exp_named_subst metasenv subst n context ens ugraph = + List.fold_right + (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 - aux -;; - + let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in + let fresh_name = + FreshNamesGenerator.mk_fresh_name ~subst + metasenv context (Cic.Name "Heta") ~typ:argty + 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'), ugraph2 -let check_accessibility metasenv i = - let module C = Cic in - let module S = CicSubstitution in - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=i) metasenv in - List.map - (function t -> - let = - S.delift canonical_context metasenv ? t - ) canonical_context -CSCSCS +(* 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,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 - let rec aux metasenv k = - function - C.Rel i -> - if i <= k then - metasenv - else - (try - match List.nth canonical_context (i-k-1) with - Some (_,C.Decl t) - | Some (_,C.Def t) -> aux metasenv k (S.lift i t) - | None -> raise RelToHiddenHypothesis - with - Failure _ -> raise OpenTerm - ) - | C.Var _ -> metasenv - | C.Meta (i,l) -> restrict canonical_context i k l metasenv - | C.Sort _ -> metasenv - | C.Implicit -> metasenv - | C.Cast (te,ty) -> - let metasenv' = aux metasenv k te in - aux metasenv' k ty - | C.Prod (_,s,t) - | C.Lambda (_,s,t) - | C.LetIn (_,s,t) -> - let metasenv' = aux metasenv k s in - aux metasenv' (k+1) t - | C.Appl l -> - List.fold_left - (function metasenv -> aux metasenv k) metasenv l - | C.Const _ - | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ -> metasenv - | C.MutCase (_,_,_,outty,t,pl) -> - let metasenv' = aux metasenv k outty in - let metasenv'' = aux metasenv' k t in - List.fold_left - (function metasenv -> aux metasenv k) metasenv'' pl - | C.Fix (i, fl) -> - let len = List.length fl in - List.fold_left - (fun metasenv f -> - let (_,_,ty,bo) = f in - let metasenv' = aux metasenv k ty in - aux metasenv' (k+len) bo - ) metasenv fl - | C.CoFix (i, fl) -> - let len = List.length fl in - List.fold_left - (fun metasenv f -> - let (_,ty,bo) = f in - let metasenv' = aux metasenv k ty in - aux metasenv' (k+len) bo - ) metasenv fl - in aux metasenv 0 -;; -*) +(* NUOVA UNIFICAZIONE *) +(* A substitution is a (int * Cic.term) list that associates a + metavariable i with its body. + A metaenv is a (int * Cic.term) list that associate a metavariable + i with is type. + fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back + 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 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 + 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,ugraph) t1 t2 -> + match t1,t2 with + None,_ + | _,None -> j+1,subst,metasenv,ugraph + | Some t1', Some t2' -> + (* First possibility: restriction *) + (* Second possibility: unification *) + (* Third possibility: convertibility *) + 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,ugraph1) + ) (1,subst,metasenv,ugraph) ln lm + with + Exit -> + raise + (UnificationFailure "1") +(* + (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))) *) + | Invalid_argument _ -> + raise + (UnificationFailure "2")) +(* + (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,ugraph1 -let unwind metasenv subst unwinded t = - let unwinded = ref unwinded in - let frozen = ref [] in - let rec um_aux metasenv = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t,metasenv - | C.Var _ as t -> t,metasenv - | C.Meta (i,l) -> - (try - S.lift_meta l (List.assoc i !unwinded), metasenv - with Not_found -> - if List.mem i !frozen then raise OccurCheck - else - let saved_frozen = !frozen in - frozen := i::!frozen ; - let res = - try - let t = List.assoc i subst in - let t',metasenv' = um_aux metasenv t in - let _,metasenv'' = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=i) metasenv - in -prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ; -List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; -prerr_endline " - (* not constrained variable, i.e. free in subst*) - let l',metasenv' = - List.fold_right - (fun t (tl,metasenv) -> - match t with - None -> None::tl,metasenv - | Some t -> - let t',metasenv' = um_aux metasenv t in - (Some t')::tl, metasenv' - ) l ([],metasenv) - in - C.Meta (i,l'), metasenv' - in - frozen := saved_frozen ; - res - ) - | C.Sort _ - | C.Implicit as t -> t,metasenv - | C.Cast (te,ty) -> - let te',metasenv' = um_aux metasenv te in - let ty',metasenv'' = um_aux metasenv' ty in - C.Cast (te',ty'),metasenv'' - | C.Prod (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.Prod (n, s', t'), metasenv'' - | C.Lambda (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.Lambda (n, s', t'), metasenv'' - | C.LetIn (n,s,t) -> - let s',metasenv' = um_aux metasenv s in - let t',metasenv'' = um_aux metasenv' t in - C.LetIn (n, s', t'), metasenv'' - | C.Appl (he::tl) -> - let tl',metasenv' = - List.fold_right - (fun t (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - t'::tl, metasenv' - ) tl ([],metasenv) + | (C.Meta (n,_), C.Meta (m,_)) when n>m -> + fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph + | (C.Meta (n,l), t) + | (t, C.Meta (n,l)) -> + let swap = + match t1,t2 with + C.Meta (n,_), C.Meta (m,_) when n < m -> false + | _, C.Meta _ -> false + | _,_ -> true + in + 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 ugraph = + fo_unif_subst test_equality_only subst context metasenv + (lower m1 m2) (upper m1 m2) ugraph in +(* begin - match um_aux metasenv' he with - (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv'' - | (he', metasenv'') -> C.Appl (he'::tl'),metasenv'' + try + let (_, oldt) = CicMetaSubst.lookup_subst n subst in + let lifted_oldt = S.lift_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.lift_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.lift_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 - | C.Appl _ -> assert false - | C.Const _ - | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ as t -> t,metasenv - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - let outty',metasenv' = um_aux metasenv outty in - let t',metasenv'' = um_aux metasenv' t in - let pl',metasenv''' = - List.fold_right - (fun p (pl,metasenv) -> - let p',metasenv' = um_aux metasenv p in - p'::pl, metasenv' - ) pl ([],metasenv'') +*) + begin + 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.lift_meta l meta_type) ugraph1 + with + UnificationFailure msg + | Uncertain msg -> + prerr_endline msg;raise (UnificationFailure msg) + | AssertFailure _ -> + prerr_endline "siamo allo huge hack"; + (* 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) *) + (subst, metasenv,ugraph)) in + let t',metasenv,subst = + try + 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,_) = CicUtil.lookup_subst n subst in + let lifted_oldt = S.lift_meta l oldt in + fo_unif_subst_ordered + test_equality_only subst context metasenv t lifted_oldt ugraph2 + with + CicUtil.Subst_not_found _ -> + 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, 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 ugraph + else + raise (UnificationFailure "3") + (* (sprintf + "Can't unify %s with %s due to different constants" + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + | 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 ugraph + else + raise (UnificationFailure "4") + (* (sprintf + "Can't unify %s with %s due to different inductive principles" + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + | C.MutConstruct (uri1,i1,j1,exp_named_subst1), + 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 ugraph + else + raise (UnificationFailure "5") + (* (sprintf + "Can't unify %s with %s due to different inductive constructors" + (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 ugraph + | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only + subst context metasenv t1 te ugraph + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv',ugraph1 = + fo_unif_subst true subst context metasenv s1 s2 ugraph in - C.MutCase (sp, cookingsno, i, outty', t', pl'),metasenv''' - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl,metasenv' = - List.fold_right - (fun (name, i, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, i, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) + 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)) -> + let subst',metasenv',ugraph1 = + fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph in - C.Fix (i, liftedfl),metasenv' - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl,metasenv' = - List.fold_right - (fun (name, ty, bo) (fl,metasenv) -> - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, ty', bo')::fl,metasenv'' - ) fl ([],metasenv) + 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) 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 = + function + (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) -> + let he'' = CicSubstitution.subst he' t in + if tl' = [] then + he'' + 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,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, _ 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 reduced = beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv reduced t2 ugraph + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + 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 reduced = beta_reduce (Cic.Appl (lifted::args)) in + fo_unif_subst + test_equality_only + subst context metasenv t1 reduced ugraph + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded,ugraph1 = + beta_expand_many + 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 ugraph1) + | _,_ -> +(* WAS BEFORE ----- +<<<<<<< cicUnification.ml + subst,metasenv,t1,t2,ugraph in - C.CoFix (i, liftedfl),metasenv' - in - let t',metasenv' = um_aux metasenv t in - t',metasenv',!unwinded -;; - -(* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) -(* performs as (apply_subst subst t) until it finds an application of *) -(* (META [meta_to_reduce]) that, once unwinding is performed, creates *) -(* a new beta-redex; in this case up to [reductions_no] consecutive *) -(* beta-reductions are performed. *) -(* Hint: this function is usually called when [reductions_no] *) -(* eta-expansions have been performed and the head of the new *) -(* application has been unified with (META [meta_to_reduce]): *) -(* during the unwinding the eta-expansions are undone. *) - -let apply_subst_reducing subst meta_to_reduce t = - let unwinded = ref subst in - let rec um_aux = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ - | C.Var _ as t -> t - | C.Meta (i,l) as t -> + 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 (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)) 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) ugraph1 + in + fo_unif_l + test_equality_only subst metasenv (lr1, lr2) ugraph)(**) + | (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))-> + 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 - S.lift_meta l (List.assoc i !unwinded) - with Not_found -> - C.Meta (i,l)) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux s, um_aux t) - | C.Appl (he::tl) -> - let tl' = List.map um_aux tl in - let t' = - match um_aux he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - in - begin - match meta_to_reduce,he with - Some (mtr,reductions_no), C.Meta (m,_) when m = mtr -> - let rec beta_reduce = - function - (n,(C.Appl (C.Lambda (_,_,t)::he'::tl'))) when n > 0 -> - let he'' = CicSubstitution.subst he' t in - if tl' = [] then - he'' - else - beta_reduce (n-1,C.Appl(he''::tl')) - | (_,t) -> t - in - beta_reduce (reductions_no,t') - | _,_ -> t' - end - | C.Appl _ -> assert false - | C.Const _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - C.MutCase (sp, cookingsno, i, um_aux outty, um_aux t, - List.map um_aux pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) - fl - in - C.Fix (i, liftedfl) - | C.CoFix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) - fl + List.fold_left2 + (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")) + (* (sprintf + "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,ugraph + else + raise (UnificationFailure "6") + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + | (C.Sort _ ,_) | (_, C.Sort _) + | (C.Const _, _) | (_, C.Const _) + | (C.MutInd _, _) | (_, C.MutInd _) + | (C.MutConstruct _, _) | (_, C.MutConstruct _) + | (C.Fix _, _) | (_, C.Fix _) + | (C.CoFix _, _) | (_, C.CoFix _) -> + 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))) *) + | (_,_) -> + let b,ugraph1 = + R.are_convertible ~subst ~metasenv context t1 t2 ugraph in - C.CoFix (i, liftedfl) - in - um_aux t -;; - -(* UNWIND THE MGU INSIDE THE MGU *) -let unwind_subst metasenv subst = - let identity_relocation_list_for_metavariable i = - let (_,canonical_context,_) = - List.find (function (m,_,_) -> m=i) metasenv - in - let canonical_context_length = List.length canonical_context in - let rec aux = - function - n when n > canonical_context_length -> [] - | n -> (Some (Cic.Rel n))::(aux (n+1)) - in - aux 1 - in - List.fold_left - (fun (unwinded,metasenv) (i,_) -> - let identity_relocation_list = - identity_relocation_list_for_metavariable i - in - let (_,metasenv',subst') = - unwind metasenv subst unwinded (Cic.Meta (i,identity_relocation_list)) - in - subst',metasenv' - ) ([],metasenv) subst -;; + 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))) *) -let apply_subst subst t = - (* metasenv will not be used nor modified. So, let's use a dummy empty one *) - let metasenv = [] in - let (t',_,_) = unwind metasenv [] subst t in - t' -;; +and fo_unif_subst_exp_named_subst test_equality_only subst context metasenv + exp_named_subst1 exp_named_subst2 ugraph += + try + List.fold_left2 + (fun (subst,metasenv,ugraph) (uri1,t1) (uri2,t2) -> + assert (uri1=uri2) ; + 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 = + String.concat " ; " + (List.map + (fun (uri,t) -> + UriManager.string_of_uri uri ^ " := " ^ (CicMetaSubst.ppterm subst t) + ) ens) + in + raise (UnificationFailure (sprintf + "Error trying to unify the two explicit named substitutions (local contexts) %s and %s: their lengths is different." (print_ens exp_named_subst1) (print_ens exp_named_subst2))) (* A substitution is a (int * Cic.term) list that associates a *) (* metavariable i with its body. *) @@ -503,12 +782,30 @@ let apply_subst subst t = (* 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 = -prerr_endline "INIZIO FASE 1" ; flush stderr ; - let subst_to_unwind,metasenv' = fo_unif_new metasenv context t1 t2 in -prerr_endline "FINE FASE 1" ; flush stderr ; -let res = - unwind_subst metasenv' subst_to_unwind -in -prerr_endline "FINE FASE 2" ; flush stderr ; res +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 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 + let ty_t1,_ = type_of_aux' metasenv subst context t1 ugraph in + CicPp.ppterm ty_t1 + with _ -> "MALFORMED") + (CicMetaSubst.ppterm subst t2) + (try + 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 ugraph + with + | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) + | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg)) ;; +