X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=cebbb9e8f68d2bc1fadc45f2fbca438fad2bf617;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=5b1d3ce1b932015736f9f06ebcef31fe20a6fcf2;hpb=211f0ab4ee4c22c98147067987874b0b5a800b5b;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 5b1d3ce1b..cebbb9e8f 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -23,610 +23,554 @@ * http://cs.unibo.it/helm/. *) -exception UnificationFailed;; -(*CSC: Vecchia unificazione: exception Impossible;;*) -exception Free;; -exception OccurCheck;; +open Printf -type substitution = (int * Cic.term) list +exception UnificationFailure of string;; +exception Uncertain of string;; +exception AssertFailure of string;; -(*CSC: Hhhmmm. Forse dovremmo spostarla in CicSubstitution dove si trova la *) -(*CSC: lift? O creare una proofEngineSubstitution? *) -(* the function delift n m un-lifts a lambda term m of n level of abstractions. - It returns an exception Free if M contains a free variable in the range 1--n *) -let delift n = - let rec deliftaux k = - let module C = Cic in - function - C.Rel m -> - if m < k then C.Rel m else - if m < k+n then raise Free - else C.Rel (m - n) - | C.Var _ as t -> t - | C.Meta _ as t -> t - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (deliftaux k te, deliftaux k ty) - | C.Prod (n,s,t) -> C.Prod (n, deliftaux k s, deliftaux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, deliftaux k s, deliftaux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, deliftaux k s, deliftaux (k+1) t) - | C.Appl l -> C.Appl (List.map (deliftaux k) l) - | 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, deliftaux k outty, deliftaux k t, - List.map (deliftaux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, deliftaux k ty, deliftaux (k+len) 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, deliftaux k ty, deliftaux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - if n = 0 then - (function t -> t) - else - deliftaux 1 +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 + | 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 = + 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 ;; -(* Questa funzione non serve piu'... per il momento la lascio *) -(* -let closed_up_to_n n m = - let rec closed_aux k = - let module C = Cic in - function - C.Rel m -> if m > k then () else raise Free - | C.Var _ - | C.Meta _ (* we assume Meta are closed up to k; note that during - meta-unfolding we shall need to properly lift the - "body" of Metavariables *) - | C.Sort _ - | C.Implicit -> () - | C.Cast (te,ty) -> closed_aux k te; closed_aux k ty - | C.Prod (n,s,t) -> closed_aux k s; closed_aux (k+1) t - | C.Lambda (n,s,t) -> closed_aux k s; closed_aux (k+1) t - | C.LetIn (n,s,t) -> closed_aux k s; closed_aux (k+1) t - | C.Appl l -> List.iter (closed_aux k) l - | C.Const _ - | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ -> () - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> - closed_aux k outty; closed_aux k t; - List.iter (closed_aux k) pl - | C.Fix (i, fl) -> - let len = List.length fl in - List.iter - (fun (name, i, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo) - fl - | C.CoFix (i, fl) -> - let len = List.length fl in - List.iter - (fun (name, ty, bo) -> closed_aux k ty; closed_aux (k+len) bo) - fl - in - if n = 0 then true - else - try closed_aux n m; true - with Free -> false -;; *) +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 + (CicSubstitution.lift n arg) t' + in + subst,metasenv,C.Rel (1 + n) + with + Uncertain _ + | UnificationFailure _ -> + match t' with + | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1) + | C.Var (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.Var (uri,exp_named_subst') + | 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) -> + let subst,metasenv,te' = aux metasenv subst n context te in + let subst,metasenv,ty' = aux metasenv subst n context ty in + subst,metasenv,C.Cast (te', ty') + | C.Prod (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + in + subst,metasenv,C.Prod (nn, s', t') + | C.Lambda (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + in + subst,metasenv,C.Lambda (nn, s', t') + | C.LetIn (nn,s,t) -> + let subst,metasenv,s' = aux metasenv subst n context s in + let subst,metasenv,t' = + aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t + in + subst,metasenv,C.LetIn (nn, s', t') + | C.Appl l -> + let subst,metasenv,revl' = + List.fold_left + (fun (subst,metasenv,appl) t -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,t'::appl + ) (subst,metasenv,[]) l + in + subst,metasenv,C.Appl (List.rev revl') + | C.Const (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.Const (uri,exp_named_subst') + | C.MutInd (uri,i,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.MutInd (uri,i,exp_named_subst') + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst,metasenv,exp_named_subst' = + aux_exp_named_subst metasenv subst n context exp_named_subst + in + subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst') + | C.MutCase (sp,i,outt,t,pl) -> + let subst,metasenv,outt' = aux metasenv subst n context outt in + let subst,metasenv,t' = aux metasenv subst n context t in + let subst,metasenv,revpl' = + List.fold_left + (fun (subst,metasenv,pl) t -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,t'::pl + ) (subst,metasenv,[]) pl + in + subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl') + | 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,CicMetaSubst.lift subst 1 t' *) + subst,metasenv,CicSubstitution.lift 1 t' + | 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) +*) (* 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 + (fun (uri,t) (subst,metasenv,l) -> + let subst,metasenv,t' = aux metasenv subst n context t in + subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) + 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 + (* 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 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 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 + 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 k t1 t2 = - match (t1, t2) with - (C.Meta n, C.Meta m) -> if n == m then subst - else let subst'= - let tn = try List.assoc n subst - with Not_found -> C.Meta n in - let tm = try List.assoc m subst - with Not_found -> C.Meta m in - (match (tn, tm) with - (C.Meta n, C.Meta m) -> if n==m then subst - else if n (n, tm)::subst - | (tn, C.Meta m) -> (m, tn)::subst - | (tn,tm) -> fo_unif_aux subst 0 tn tm) in - (* unify types first *) - let tyn = List.assoc n metasenv in - let tym = List.assoc m metasenv in - fo_unif_aux subst' 0 tyn tym - | (C.Meta n, t) - | (t, C.Meta n) -> (* unify types first *) - let t' = delift k t in - let subst' = - (try fo_unif_aux subst 0 (List.assoc n subst) t' - with Not_found -> (n, t')::subst) in - let tyn = List.assoc n metasenv in - let tyt = CicTypeChecker.type_of_aux' metasenv context t' in - fo_unif_aux subst' 0 tyn tyt - | (C.Rel _, _) - | (_, C.Rel _) - | (C.Var _, _) - | (_, C.Var _) - | (C.Sort _ ,_) - | (_, C.Sort _) - | (C.Implicit, _) - | (_, C.Implicit) -> if R.are_convertible t1 t2 then subst - else raise UnificationFailed - | (C.Cast (te,ty), t2) -> fo_unif_aux subst k te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_aux subst k t1 te - | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> - let subst' = fo_unif_aux subst k s1 s2 in - fo_unif_aux subst' (k+1) t1 t2 - | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> - let subst' = fo_unif_aux subst k s1 s2 in - fo_unif_aux subst' (k+1) t1 t2 - | (C.LetIn (_,s1,t1), t2) -> fo_unif_aux subst k (S.subst s1 t1) t2 - | (t1, C.LetIn (_,s2,t2)) -> fo_unif_aux subst k t1 (S.subst s2 t2) - | (C.Appl l1, C.Appl l2) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_l subst = function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> fo_unif_aux subst k h1 h2 - | ([h],l) - | (l,[h]) -> fo_unif_aux subst k h (C.Appl l) - | ((h1::l1),(h2::l2)) -> - let subst' = fo_unif_aux subst k h1 h2 in - fo_unif_l subst' (l1,l2) - in - fo_unif_l subst (lr1, lr2) - | (C.Const _, _) - | (_, C.Const _) - | (C.Abst _, _) - | (_, C.Abst _) - | (C.MutInd _, _) - | (_, C.MutInd _) - | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> if R.are_convertible t1 t2 then subst - else raise UnificationFailed - | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> - let subst' = fo_unif_aux subst k outt1 outt2 in - let subst'' = fo_unif_aux subst' k t1 t2 in - List.fold_left2 (function subst -> fo_unif_aux subst k) subst'' pl1 pl2 - | (C.Fix _, _) - | (_, C.Fix _) - | (C.CoFix _, _) - | (_, C.CoFix _) -> if R.are_convertible t1 t2 then subst - else raise UnificationFailed - | (_,_) -> raise UnificationFailed - in fo_unif_aux [] 0 t1 t2;; - -(* VECCHIA UNIFICAZIONE -- molto piu' bella, alas *) -(* -let fo_unif_mgu k t1 t2 mgu = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - let rec deref n = match mgu.(n) with - C.Meta m as t -> if n = m then t else (deref m) - | t -> t - in - let rec fo_unif k t1 t2 = match (t1, t2) with - (* aggiungere l'unificazione sui tipi in caso di istanziazione *) - (C.Meta n, C.Meta m) -> if n == m then () else - let t1' = deref n in - let t2' = deref m in - (* deref of metavariables ARE already delifted *) - (match (t1',t2') with - (C.Meta n, C.Meta m) -> if n = m then () else - if n < m then mgu.(m) <- t1' else - if n > m then mgu.(n) <- t2' - | (C.Meta n, _) -> mgu.(n) <- t2' - | (_, C.Meta m) -> mgu.(m) <- t1' - | (_,_) -> fo_unif k t1' t2') - | (C.Meta n, _) -> let t1' = deref n in - let t2' = try delift k t2 - with Free -> raise UnificationFailed in - (match t1' with - C.Meta n -> mgu.(n) <- t2' - | _ -> fo_unif k t1' t2') - | (_, C.Meta m) -> let t2' = deref m in - let t1' = try delift k t1 - with Free -> raise UnificationFailed in - (match t2' with - C.Meta m -> mgu.(m) <- t1' - | _ -> fo_unif k t1' t2') - | (C.Rel _, _) - | (_, C.Rel _) - | (C.Var _, _) - | (_, C.Var _) - | (C.Sort _ ,_) - | (_, C.Sort _) - | (C.Implicit, _) - | (_, C.Implicit) -> if R.are_convertible t1 t2 then () - else raise UnificationFailed - | (C.Cast (te,ty), _) -> fo_unif k te t2 - | (_, C.Cast (te,ty)) -> fo_unif k t1 te - | (C.Prod (_,s1,t1), C.Prod (_,s2,t2)) -> fo_unif k s1 s2; - fo_unif (k+1) t1 t2 - | (C.Lambda (_,s1,t1), C.Lambda (_,s2,t2)) -> fo_unif k s1 s2; - fo_unif (k+1) t1 t2 - | (C.LetIn (_,s1,t1), _) -> fo_unif k (S.subst s1 t1) t2 - | (_, C.LetIn (_,s2,t2)) -> fo_unif k t1 (S.subst s2 t2) - | (C.Appl (h1::l1), C.Appl (h2::l2)) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_aux = function - ([],l2) -> ([],l2) - | (l1,[]) -> (l1,[]) - | ((h1::l1),(h2::l2)) -> fo_unif k h1 h2; - fo_unif_aux (l1,l2) - in - (match fo_unif_aux (lr1, lr2) with - ([],[]) -> fo_unif k h1 h2 - | ([],l2) -> fo_unif k h1 (C.Appl (h2::List.rev l2)) - | (l1,[]) -> fo_unif k (C.Appl (h1::List.rev l1)) h2 - | (_,_) -> raise Impossible) - | (C.Const _, _) - | (_, C.Const _) - | (C.Abst _, _) - | (_, C.Abst _) - | (C.MutInd _, _) - | (_, C.MutInd _) - | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> print_endline "siamo qui"; flush stdout; - if R.are_convertible t1 t2 then () - else raise UnificationFailed - | (C.MutCase (_,_,_,outt1,t1,pl1), C.MutCase (_,_,_,outt2,t2,pl2))-> - fo_unif k outt1 outt2; - fo_unif k t1 t2; - List.iter2 (fo_unif k) pl1 pl2 - | (C.Fix _, _) - | (_, C.Fix _) - | (C.CoFix _, _) - | (_, C.CoFix _) -> if R.are_convertible t1 t2 then () - else raise UnificationFailed - | (_,_) -> raise UnificationFailed - in fo_unif k t1 t2;mgu ;; -*) - -(* unwind mgu mark m applies mgu to the term m; mark is an array of integers -mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding, -and is 1 if it has been succesfully unwinded. Meeting the value 2 during -the computation is an error: occur-check *) - -let unwind subst unwinded t = - let unwinded = ref unwinded in - let frozen = ref [] in - let rec um_aux k = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta i as t ->(try S.lift k (List.assoc i !unwinded) - 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' = um_aux 0 t in - unwinded := (i,t)::!unwinded ; - S.lift k t' - with - Not_found -> - (* not constrained variable, i.e. free in subst *) - C.Meta i - in - frozen := saved_frozen ; - res - ) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) - | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in - begin - match um_aux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - 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 k outty, um_aux k t, - List.map (um_aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) 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 k ty, um_aux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - um_aux 0 t,!unwinded -;; +and fo_unif_subst test_equality_only subst context metasenv t1 t2 = + let module C = Cic in + let module R = CicReduction in + let module S = CicSubstitution in + let t1 = deref subst t1 in + let t2 = deref subst t2 in + match (t1, t2) with + (C.Meta (n,ln), C.Meta (m,lm)) when n=m -> + let _,subst,metasenv = + (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") (* -let unwind_meta mgu mark = - let rec um_aux k = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else - if mark.(i)=1 then S.lift k mgu.(i) - else (match mgu.(i) with - C.Meta k as t1 -> if k = i then t - else (mark.(i) <- 2; - mgu.(i) <- (um_aux 0 t1); - mark.(i) <- 1; - S.lift k mgu.(i)) - | _ -> (mark.(i) <- 2; - mgu.(i) <- (um_aux 0 mgu.(i)); - mark.(i) <- 1; - S.lift k mgu.(i))) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) - | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in - begin - match um_aux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - 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 k outty, um_aux k t, - List.map (um_aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) 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 k ty, um_aux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - um_aux 0 -;; -*) - -(* 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 k = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta i as t -> - (try - S.lift k (List.assoc i !unwinded) - with Not_found -> - C.Meta i) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) - | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in - let t' = - match um_aux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - in - begin - match meta_to_reduce with - Some (mtr,reductions_no) when he = C.Meta 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 k outty, um_aux k t, - List.map (um_aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) bo)) - fl + (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) + | (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 - 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 k ty, um_aux (k+len) bo)) - fl + 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 - C.CoFix (i, liftedfl) - in - um_aux 0 t -;; - -(* unwind mgu mark mm m applies mgu to the term m; mark is an array of integers -mark.(n) = 0 if the term has not been unwinded, is 2 if it is under uwinding, -and is 1 if it has been succesfully unwinded. Meeting the value 2 during -the computation is an error: occur-check. When the META mm is to be unfolded -and it is applied to something, one-step beta reduction is performed just -after the unfolding. *) - -(* -let unwind_meta_reducing mgu mark meta_to_reduce = - let rec um_aux k = - let module C = Cic in - let module S = CicSubstitution in - function - C.Rel _ as t -> t - | C.Var _ as t -> t - | C.Meta i as t -> if mark.(i)=2 then raise OccurCheck else - if mark.(i)=1 then S.lift k mgu.(i) - else (match mgu.(i) with - C.Meta k as t1 -> if k = i then t - else (mark.(i) <- 2; - mgu.(i) <- (um_aux 0 t1); - mark.(i) <- 1; - S.lift k mgu.(i)) - | _ -> (mark.(i) <- 2; - mgu.(i) <- (um_aux 0 mgu.(i)); - mark.(i) <- 1; - S.lift k mgu.(i))) - | C.Sort _ as t -> t - | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (um_aux k te, um_aux k ty) - | C.Prod (n,s,t) -> C.Prod (n, um_aux k s, um_aux (k+1) t) - | C.Lambda (n,s,t) -> C.Lambda (n, um_aux k s, um_aux (k+1) t) - | C.LetIn (n,s,t) -> C.LetIn (n, um_aux k s, um_aux (k+1) t) - | C.Appl (he::tl) -> - let tl' = List.map (um_aux k) tl in - let t' = - match um_aux k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') - in begin - match t', meta_to_reduce with - (C.Appl (C.Lambda (n,s,t)::he'::tl')),Some mtr - when he = C.Meta mtr -> -(*CSC: Sbagliato!!! Effettua beta riduzione solo del primo argomento - *CSC: mentre dovrebbe farla dei primi n, dove n sono quelli eta-astratti -*) - C.Appl((CicSubstitution.subst he' t)::tl') - | _ -> t' + 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 + (* 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.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 k outty, um_aux k t, - List.map (um_aux k) pl) - | C.Fix (i, fl) -> - let len = List.length fl in - let liftedfl = - List.map - (fun (name, i, ty, bo) -> (name, i, um_aux k ty, um_aux (k+len) 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 k ty, um_aux (k+len) bo)) - fl - in - C.CoFix (i, liftedfl) - in - um_aux 0 -;; *) + | (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 "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 + 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 + 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 + | (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) -> + (* 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 -> + (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 + [],_ + | _,[] -> 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 "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 t1 = t2 || R.are_convertible ~subst ~metasenv context t1 t2 then + subst, metasenv + else + raise (UnificationFailure "7") + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) + | (_,_) -> + if R.are_convertible ~subst ~metasenv context t1 t2 then + subst, metasenv + else + raise (UnificationFailure "8") + (* (sprintf + "Can't unify %s with %s because they are not convertible" + (CicMetaSubst.ppterm subst t1) (CicMetaSubst.ppterm subst t2))) *) -(* UNWIND THE MGU INSIDE THE MGU *) -(* let unwind mgu = - let mark = Array.make (Array.length mgu) 0 in - Array.iter (fun x -> let foo = unwind_meta mgu mark x in ()) mgu; mgu;; *) +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))) -let unwind_subst subst = - List.fold_left - (fun unwinded (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst -;; +(* 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 apply_subst subst t = - fst (unwind [] subst t) +let fo_unif_subst subst context metasenv t1 t2 = + 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) + 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) + (CicMetaSubst.ppsubst 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)) ;; -(* 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 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. *) -let fo_unif metasenv context t1 t2 = - let subst_to_unwind = fo_unif_new metasenv context t1 t2 in - unwind_subst subst_to_unwind -;;