X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;fp=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=0000000000000000000000000000000000000000;hp=35eb18f450974d61fc238b77d3f985203b249d6b;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml deleted file mode 100644 index 35eb18f45..000000000 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ /dev/null @@ -1,311 +0,0 @@ -(* Copyright (C) 2000, HELM Team. - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. - *) - -open Printf - -exception UnificationFailure of string;; -exception Uncertain of string;; -exception AssertFailure of string;; - -let debug_print = prerr_endline - -let type_of_aux' metasenv subst context term = - try - CicMetaSubst.type_of_aux' metasenv subst context term - 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))) - -(* 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 rec fo_unif_subst test_equality_only subst context metasenv t1 t2 = - let module C = Cic in - let module R = CicMetaSubst in - let module S = CicSubstitution 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))) - | (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) - | (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 = - fo_unif_subst test_equality_only subst context metasenv - (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'' = - 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.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 - "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 - else - raise (UnificationFailure (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 - else - raise (UnificationFailure (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 - | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only - subst context metasenv t1 te - | (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 - | (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 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_subst - test_equality_only 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 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]) -> - 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) - | (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 - (try - List.fold_left2 - (function (subst,metasenv) -> - fo_unif_subst test_equality_only subst context metasenv - ) (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 _) - | (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 - subst, metasenv - else - raise (UnificationFailure (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 context t1 t2 then - subst, metasenv - else - raise (UnificationFailure (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 -= - try - List.fold_left2 - (fun (subst,metasenv) (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 - 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. *) -(* metasenv is of type Cic.metasenv *) -(* fo_unif takes a metasenv, a context, two terms t1 and t2 and gives back *) -(* 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_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" - (CicMetaSubst.ppterm subst t1) - (try - CicPp.ppterm (type_of_aux' metasenv subst context t1) - with _ -> "MALFORMED") - (CicMetaSubst.ppterm subst t2) - (try - CicPp.ppterm (type_of_aux' metasenv subst context t2) - with _ -> "MALFORMED") - (CicMetaSubst.ppcontext subst context) - (CicMetaSubst.ppmetasenv metasenv subst) msg - in - try - fo_unif_subst false subst context metasenv t1 t2 - with - | AssertFailure msg -> raise (AssertFailure (enrich_msg msg)) - | UnificationFailure msg -> raise (UnificationFailure (enrich_msg msg)) -;; -