X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=cebbb9e8f68d2bc1fadc45f2fbca438fad2bf617;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=8a1f4c43e8aef1d5fd25feb63f3a92c2ce829dcf;hpb=fb0f22004d533abca8d157ed89665dbf1041e0e2;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 8a1f4c43e..cebbb9e8f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -32,6 +32,21 @@ exception AssertFailure of string;; let debug_print = prerr_endline let type_of_aux' metasenv subst context term = + try + CicTypeChecker.type_of_aux' ~subst metasenv context term + 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);; +(* try CicMetaSubst.type_of_aux' metasenv subst context term with @@ -41,16 +56,28 @@ let type_of_aux' metasenv subst context term = "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))) + (CicMetaSubst.ppmetasenv metasenv subst) msg))) *) -let rec eta_expand test_equality_only metasenv subst context t arg = - let module T = CicTypeChecker in +let rec deref subst = + 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 = let module S = CicSubstitution in let module C = Cic in let rec aux metasenv subst n context t' = try let subst,metasenv = - fo_unif_subst test_equality_only subst context metasenv arg t' + fo_unif_subst test_equality_only subst context metasenv + (CicSubstitution.lift n arg) t' in subst,metasenv,C.Rel (1 + n) with @@ -63,12 +90,32 @@ let rec eta_expand test_equality_only metasenv subst context t arg = aux_exp_named_subst metasenv subst n context exp_named_subst in subst,metasenv,C.Var (uri,exp_named_subst') - | C.Meta (i,l) as t-> - (try - let t' = List.assoc i subst in - aux metasenv subst n context t' - with - Not_found -> subst,metasenv,t) + | 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) + (* + 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 + in + (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.Cast (te,ty) -> @@ -137,7 +184,8 @@ let rec eta_expand test_equality_only metasenv subst context t arg = fl in C.Fix (i, substitutedfl) -*) subst,metasenv,CicMetaSubst.lift subst 1 t' +*) (* subst,metasenv,CicMetaSubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' | C.CoFix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -147,7 +195,8 @@ let rec eta_expand test_equality_only metasenv subst context t arg = fl in C.CoFix (i, substitutedfl) -*) subst,metasenv,CicMetaSubst.lift subst 1 t' +*) (* subst,metasenv,CicMetasubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' and aux_exp_named_subst metasenv subst n context ens = List.fold_right @@ -155,21 +204,27 @@ let rec eta_expand test_equality_only metasenv subst context t arg = let subst,metasenv,t' = aux metasenv subst n context t in subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) in - let argty = - T.type_of_aux' metasenv context arg - in + let argty = type_of_aux' metasenv subst context arg in let fresh_name = FreshNamesGenerator.mk_fresh_name metasenv context (Cic.Name "Heta") ~typ:argty in let subst,metasenv,t' = aux metasenv subst 0 context t in - subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + (* prova *) + (* old + subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + *) + subst, metasenv, C.Lambda (fresh_name,argty,t') -and eta_expand_many test_equality_only metasenv subst context t = - List.fold_left - (fun (subst,metasenv,t) arg -> - eta_expand test_equality_only metasenv subst context t arg - ) (subst,metasenv,t) +and beta_expand_many test_equality_only metasenv subst context t args = + let subst,metasenv,hd = + 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 (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a @@ -182,45 +237,57 @@ and eta_expand_many test_equality_only metasenv subst context t = and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in - let module R = CicMetaSubst 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 ok,subst,metasenv = - try - List.fold_left2 - (fun (b,subst,metasenv) t1 t2 -> - if b then true,subst,metasenv else - match t1,t2 with - None,_ - | _,None -> true,subst,metasenv - | Some t1', Some t2' -> - (* First possibility: restriction *) - (* Second possibility: unification *) - (* Third possibility: convertibility *) - if R.are_convertible subst context t1' t2' then - true,subst,metasenv - else - (try - let subst,metasenv = - fo_unif_subst - test_equality_only subst context metasenv t1' t2' - in - true,subst,metasenv - with - Not_found -> false,subst,metasenv) - ) (true,subst,metasenv) 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 - 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 = + (try + List.fold_left2 + (fun (j,subst,metasenv) t1 t2 -> + match t1,t2 with + None,_ + | _,None -> j+1,subst,metasenv + | 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 _ -> +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 + 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 | (C.Meta (n,_), C.Meta (m,_)) when n>m -> fo_unif_subst test_equality_only subst context metasenv t2 t1 | (C.Meta (n,l), t) @@ -236,79 +303,90 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let fo_unif_subst_ordered test_equality_only subst context metasenv m1 m2 = fo_unif_subst test_equality_only subst context metasenv - (lower m1 m2) (upper m1 m2) + (lower m1 m2) (upper m1 m2) in - let subst'',metasenv' = - try - let oldt = (List.assoc 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 - with Not_found -> - 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'' = + begin + let subst,metasenv = + let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in + (try + let tyt = type_of_aux' metasenv subst context t in + fo_unif_subst + test_equality_only + subst context metasenv tyt (S.lift_meta l meta_type) + 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)) 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'' = 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' - in - (n, t'')::subst', metasenv' - in - let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in - (try - let tyt = - type_of_aux' metasenv' subst'' context t - in - fo_unif_subst - test_equality_only - subst'' context metasenv' tyt (S.lift_meta l meta_type) - 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')) + 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' + 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 + with + CicUtil.Subst_not_found _ -> + let (_, context, _) = CicUtil.lookup_meta n metasenv in + let subst = (n, (context, t'')) :: subst in + let metasenv = + List.filter (fun (m,_,_) -> not (n = m)) metasenv in + subst, metasenv + 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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "3") + (* (sprintf "Can't unify %s with %s due to different constants" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "4") + (* (sprintf "Can't unify %s with %s due to different inductive principles" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (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 else - raise (UnificationFailure (sprintf + raise (UnificationFailure "5") + (* (sprintf "Can't unify %s with %s due to different inductive constructors" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (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 @@ -331,28 +409,55 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> - let subst,metasenv,t1',t2' = - match l1,l2 with - (* 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. - *) - C.Meta (i,l)::args, _ -> - let subst,metasenv,t2' = - eta_expand_many test_equality_only metasenv subst context t2 args - in - subst,metasenv,t1,t2' + (* 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 + (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 + with (Invalid_argument msg) -> raise (UnificationFailure msg)) + | C.Meta (i,l)::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 reduced t2 + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded = + 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 -> - let subst,metasenv,t1' = - eta_expand_many test_equality_only metasenv subst context t1 args - in - subst,metasenv,t1',t2 - | _,_ -> subst,metasenv,t1,t2 - in - begin - match t1',t2' with - C.Appl l1, C.Appl l2 -> - let lr1 = List.rev l1 in + (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 + with CicUtil.Subst_not_found _ -> + let subst,metasenv,beta_expanded = + beta_expand_many + test_equality_only metasenv subst context t1 args in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded) + | _,_ -> + let lr1 = List.rev l1 in let lr2 = List.rev l2 in let rec fo_unif_l test_equality_only subst metasenv = function @@ -362,17 +467,15 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv h1 h2 | ([h],l) | (l,[h]) -> - fo_unif_subst - test_equality_only subst context metasenv h (C.Appl (List.rev l)) + 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 in fo_unif_l test_equality_only subst' metasenv' (l1,l2) in - fo_unif_l test_equality_only subst metasenv (lr1, lr2) - | _ -> assert false - end + fo_unif_l test_equality_only subst metasenv (lr1, lr2) ) | (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 @@ -385,28 +488,38 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; ) (subst'',metasenv'') pl1 pl2 with Invalid_argument _ -> - raise (UnificationFailure (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 _) + 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 + 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 R.are_convertible subst context t1 t2 then + if t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then subst, metasenv else - raise (UnificationFailure (sprintf + raise (UnificationFailure "7") + (* (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) | (_,_) -> - if R.are_convertible subst context t1 t2 then + if R.are_convertible ~subst ~metasenv context t1 t2 then subst, metasenv else - raise (UnificationFailure (sprintf + raise (UnificationFailure "8") + (* (sprintf "Can't unify %s with %s because they are not convertible" - (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) + (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 @@ -440,8 +553,8 @@ let fo_unif metasenv context t1 t2 = fo_unif_subst false [] context metasenv t1 t2 ;; let fo_unif_subst subst context metasenv t1 t2 = - let enrich_msg msg = - sprintf "Unification error unifying %s of type %s with %s of type %s in context\n%s\nand metasenv\n%s\nbecause %s" + 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) @@ -451,7 +564,8 @@ let fo_unif_subst subst context metasenv t1 t2 = CicPp.ppterm (type_of_aux' metasenv subst context t2) with _ -> "MALFORMED") (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) msg + (CicMetaSubst.ppmetasenv metasenv subst) + (CicMetaSubst.ppsubst subst) msg in try fo_unif_subst false subst context metasenv t1 t2