X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;fp=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=0000000000000000000000000000000000000000;hb=3ef089a4c58fbe429dd539af6215991ecbe11ee2;hp=f7c19073b015755c6be36edceffc8d708db4d82d;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml deleted file mode 100644 index f7c19073b..000000000 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ /dev/null @@ -1,703 +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/. - *) - -exception UnificationFailed;; -exception Free;; -exception OccurCheck;; -exception RelToHiddenHypothesis;; -exception OpenTerm;; - -(**** DELIFT ****) - -(* the delift function takes in input an ordered list of integers [n1,...,nk] - and a term t, and relocates rel(nk) to k. Typically, the list of integers - is a parameter of a metavariable occurrence. *) - -exception NotInTheList;; - -let position n = - let rec aux k = - function - [] -> raise NotInTheList - | (Some (Cic.Rel m))::_ when m=n -> k - | _::tl -> aux (k+1) tl in - aux 1 -;; - -let restrict to_be_restricted = - let rec erase i n = - function - [] -> [] - | _::tl when List.mem (n,i) to_be_restricted -> - None::(erase (i+1) n tl) - | he::tl -> he::(erase (i+1) n tl) in - let rec aux = - function - [] -> [] - | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in - aux -;; - - -let delift context metasenv l t = - let module S = CicSubstitution in - let to_be_restricted = ref [] in - let rec deliftaux k = - let module C = Cic in - function - C.Rel m -> - if m <=k then - C.Rel m (*CSC: che succede se c'e' un Def? Dovrebbe averlo gia' *) - (*CSC: deliftato la regola per il LetIn *) - else - (match List.nth context (m-k-1) with - Some (_,C.Def t) -> deliftaux k (S.lift m t) - | Some (_,C.Decl t) -> - (* It may augment to_be_restricted *) - ignore (deliftaux k (S.lift m t)) ; - C.Rel ((position (m-k) l) + k) - | None -> raise RelToHiddenHypothesis) - | C.Var (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Var (uri,exp_named_subst') - | C.Meta (i, l1) as t -> - let rec deliftl j = - function - [] -> [] - | None::tl -> None::(deliftl (j+1) tl) - | (Some t)::tl -> - let l1' = (deliftl (j+1) tl) in - try - Some (deliftaux k t)::l1' - with - RelToHiddenHypothesis - | NotInTheList -> - to_be_restricted := (i,j)::!to_be_restricted ; None::l1' - in - let l' = deliftl 1 l1 in - C.Meta(i,l') - | 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 (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> uri,deliftaux k t) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, 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 - let res = deliftaux 0 t in - res, restrict !to_be_restricted metasenv -;; - -(**** END OF DELIFT ****) - -type substitution = (int * Cic.term) list - -(* 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 subst context metasenv t1 t2 = - let module C = Cic in - let module R = CicReduction in - let module S = CicSubstitution in - 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 - in - if ok then subst,metasenv else raise UnificationFailed - | (C.Meta (n,l), C.Meta (m,_)) when n>m -> - fo_unif_subst 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_subst subst context metasenv lifted_oldt t - with Not_found -> - let t',metasenv' = delift context metasenv l t in - (n, t')::subst, metasenv' - in - let (_,_,meta_type) = - List.find (function (m,_,_) -> m=n) metasenv' in - let tyt = CicTypeChecker.type_of_aux' metasenv' context t in - fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt - | (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 subst context metasenv - exp_named_subst1 exp_named_subst2 - else - raise UnificationFailed - | 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 subst context metasenv - exp_named_subst1 exp_named_subst2 - else - raise UnificationFailed - | 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 subst context metasenv - exp_named_subst1 exp_named_subst2 - else - raise UnificationFailed - | (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_subst subst context metasenv te t2 - | (t1, C.Cast (te,ty)) -> fo_unif_subst subst context metasenv t1 te - | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> - let subst',metasenv' = fo_unif_subst subst context metasenv s1 s2 in - fo_unif_subst subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 - | (C.LetIn (_,s1,t1), t2) - | (t2, C.LetIn (_,s1,t1)) -> - fo_unif_subst 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_subst subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> - fo_unif_subst subst context metasenv h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_subst subst context metasenv h1 h2 - in - fo_unif_l subst' metasenv' (l1,l2) - in - fo_unif_l subst metasenv (lr1, lr2) - | (C.Const _, _) - | (_, C.Const _) - | (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_subst subst context metasenv outt1 outt2 in - let subst'',metasenv'' = - fo_unif_subst subst' context metasenv' t1 t2 in - List.fold_left2 - (function (subst,metasenv) -> - fo_unif_subst 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 - | (_,_) -> - if R.are_convertible context t1 t2 then - subst, metasenv - else - raise UnificationFailed - -and fo_unif_subst_exp_named_subst 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 subst context metasenv t1 t2 - ) (subst,metasenv) exp_named_subst1 exp_named_subst2 -with -e -> -let uri = UriManager.uri_of_string "cic:/dummy.var" in -prerr_endline ("@@@: " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst1)) ^ -" <==> " ^ CicPp.ppterm (Cic.Var (uri,exp_named_subst2))) ; raise e -;; - -(*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. *) - -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) - in - aux -;; - - -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 = - delift canonical_context metasenv ? t - ) canonical_context -CSCSCS - - - - 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.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 -;; -*) - - -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 - delift canonical_context metasenv' l t' - in - unwinded := (i,t')::!unwinded ; - S.lift_meta l t', metasenv' - with - Not_found -> - (* 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) - in - begin - match um_aux metasenv' he with - (C.Appl l, metasenv'') -> C.Appl (l@tl'),metasenv'' - | (he', metasenv'') -> C.Appl (he'::tl'),metasenv'' - end - | C.Appl _ -> assert false - | C.Const (uri,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.Const (uri,exp_named_subst'),metasenv' - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.MutInd (uri,typeno,exp_named_subst'),metasenv' - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst', metasenv' = - List.fold_right - (fun (uri,t) (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - (uri,t')::tl, metasenv' - ) exp_named_subst ([],metasenv) - in - C.MutConstruct (uri,typeno,consno,exp_named_subst'),metasenv' - | C.MutCase (sp,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'') - in - C.MutCase (sp, 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) - 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) - 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 -> - (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 (uri,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst - in - C.Const (uri,exp_named_subst') - | C.MutInd (uri,typeno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst - in - C.MutInd (uri,typeno,exp_named_subst') - | C.MutConstruct (uri,typeno,consno,exp_named_subst) -> - let exp_named_subst' = - List.map (function (uri,t) -> (uri,um_aux t)) exp_named_subst - in - C.MutConstruct (uri,typeno,consno,exp_named_subst') - | C.MutCase (sp,i,outty,t,pl) -> - C.MutCase (sp, 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 - 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 -;; - -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' -;; - -(* 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 = -prerr_endline "INIZIO FASE 1" ; flush stderr ; - let subst_to_unwind,metasenv' = fo_unif_subst [] context metasenv 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 -;;