X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=cebbb9e8f68d2bc1fadc45f2fbca438fad2bf617;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=e6213d6af8895d0b0cc3c1ea6a726b18eec00e8d;hpb=3db0a84a64f014fa10c4b439c62cb3eef017ea7a;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index e6213d6af..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,7 +56,19 @@ 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 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 @@ -49,8 +76,8 @@ let rec beta_expand test_equality_only metasenv subst context t arg = let rec aux metasenv subst n context t' = try let subst,metasenv = - fo_unif_subst test_equality_only subst context metasenv - (CicSubstitution.lift n 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,24 +90,32 @@ let rec beta_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') = CicMetaSubst.lookup_subst i subst in - aux metasenv subst n context (CicSubstitution.lift_meta l t') - with CicMetaSubst.SubstNotFound _ -> - let (subst, metasenv, context, local_context) = - List.fold_left - (fun (subst, metasenv, context, local_context) t -> - match t with + | 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)) - (subst, metasenv, context, []) l - in - (subst, metasenv, C.Meta (i, local_context))) + (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) -> @@ -149,7 +184,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,CicMetaSubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' | C.CoFix (i,fl) -> (*CSC: not implemented let tylen = List.length fl in @@ -159,7 +195,8 @@ 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,CicMetasubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' and aux_exp_named_subst metasenv subst n context ens = List.fold_right @@ -173,13 +210,21 @@ let rec beta_expand test_equality_only metasenv subst context t arg = metasenv context (Cic.Name "Heta") ~typ:argty in let subst,metasenv,t' = aux metasenv subst 0 context t in + (* prova *) + (* old subst, metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + *) + subst, metasenv, C.Lambda (fresh_name,argty,t') -and beta_expand_many test_equality_only metasenv subst context t = - List.fold_left - (fun (subst,metasenv,t) arg -> - beta_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 @@ -192,45 +237,57 @@ and beta_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) @@ -248,101 +305,88 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = fo_unif_subst test_equality_only subst context metasenv (lower m1 m2) (upper m1 m2) in - begin - try - let (_, oldt) = CicMetaSubst.lookup_subst n subst in - let lifted_oldt = S.lift_meta l oldt in - let ty_lifted_oldt = - type_of_aux' metasenv subst context lifted_oldt - in - let tyt = type_of_aux' metasenv subst context t in - let (subst, metasenv) = - fo_unif_subst_ordered test_equality_only subst context metasenv - tyt ty_lifted_oldt - in - fo_unif_subst_ordered - test_equality_only subst context metasenv t lifted_oldt - with CicMetaSubst.SubstNotFound _ -> - (* First of all we unify the type of the meta with the type of the term *) + 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 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)) - 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 - (* 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 - 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 -(* (n,t'')::subst, metasenv *) - end + 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 + (* 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 @@ -365,31 +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 - C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j -> - subst,metasenv,t1,t2 - (* 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 + (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, _ -> - let subst,metasenv,t2' = - beta_expand_many test_equality_only metasenv subst context t2 args - in - subst,metasenv,t1,t2' + (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' = - beta_expand_many test_equality_only metasenv subst context t1 args - in - subst,metasenv,t1',t2 + (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) | _,_ -> - subst,metasenv,t1,t2 - 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 @@ -407,9 +475,7 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; 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 @@ -422,34 +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)))) + 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 (sprintf + raise (UnificationFailure "6") + (* (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))) *) | (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 || 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 @@ -483,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) @@ -494,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