X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=2f27bea85adac6a996c5152d40d5b7635996d1c0;hb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;hp=4126d04464e6626a1b1a0c4e32389138709cf2d7;hpb=a61f397a3ea3acaf95a04a2aafbf1d3f223a2755;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 4126d0446..2f27bea85 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -26,103 +26,63 @@ exception UnificationFailed;; exception Free;; exception OccurCheck;; +exception RelToHiddenHypothesis;; +exception OpenTerm;; type substitution = (int * Cic.term) list -(*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 -;; - (* 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 = + let rec fo_unif_aux subst context metasenv 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.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_aux 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_aux subst context metasenv lifted_oldt t + with Not_found -> +prerr_endline ("DELIFT2(" ^ CicPp.ppterm t ^ ")") ; flush stderr ; +List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; +prerr_endline " m=n) metasenv' in + let tyt = CicTypeChecker.type_of_aux' metasenv' context t in + fo_unif_aux subst' context metasenv' (S.lift_meta l meta_type) tyt | (C.Rel _, _) | (_, C.Rel _) | (C.Var _, _) @@ -130,32 +90,38 @@ let fo_unif_new metasenv context t1 t2 = | (C.Sort _ ,_) | (_, C.Sort _) | (C.Implicit, _) - | (_, C.Implicit) -> if R.are_convertible context 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.Implicit) -> + if R.are_convertible context t1 t2 then subst, metasenv + else raise UnificationFailed + | (C.Cast (te,ty), t2) -> fo_unif_aux subst context metasenv te t2 + | (t1, C.Cast (te,ty)) -> fo_unif_aux subst context metasenv t1 te + | (C.Prod (n1,s1,t1), C.Prod (_,s2,t2)) -> + let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in + fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) -> + let subst',metasenv' = fo_unif_aux subst context metasenv s1 s2 in + fo_unif_aux subst' ((Some (n1,(C.Decl s1)))::context) metasenv' t1 t2 + | (C.LetIn (_,s1,t1), t2) + | (t2, C.LetIn (_,s1,t1)) -> + fo_unif_aux 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 = 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) + 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_aux subst context metasenv h1 h2 + | ([h],l) + | (l,[h]) -> + fo_unif_aux subst context metasenv h (C.Appl (List.rev l)) + | ((h1::l1),(h2::l2)) -> + let subst', metasenv' = + fo_unif_aux 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.Abst _, _) @@ -163,94 +129,258 @@ let fo_unif_new metasenv context t1 t2 = | (C.MutInd _, _) | (_, C.MutInd _) | (C.MutConstruct _, _) - | (_, C.MutConstruct _) -> if R.are_convertible context t1 t2 then subst - else raise UnificationFailed + | (_, 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' = 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 + let subst', metasenv' = + fo_unif_aux subst context metasenv outt1 outt2 in + let subst'',metasenv'' = + fo_unif_aux subst' context metasenv' t1 t2 in + List.fold_left2 + (function (subst,metasenv) -> + fo_unif_aux subst context metasenv + ) (subst'',metasenv'') pl1 pl2 | (C.Fix _, _) | (_, C.Fix _) | (C.CoFix _, _) - | (_, C.CoFix _) -> if R.are_convertible context t1 t2 then subst - else raise UnificationFailed + | (_, C.CoFix _) -> + if R.are_convertible context t1 t2 then subst, metasenv + else raise UnificationFailed | (_,_) -> raise UnificationFailed - in fo_unif_aux [] 0 t1 t2;; + in fo_unif_aux [] context metasenv t1 t2;; + +(*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 = + S.delift canonical_context metasenv ? t + ) canonical_context +CSCSCS -(* 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 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.Abst _ + | 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 k = + let rec um_aux metasenv = 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.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 +prerr_endline ("DELIFT(" ^ CicPp.ppterm t' ^ ")") ; flush stderr ; +List.iter (function (Some t) -> prerr_endline ("l: " ^ CicPp.ppterm t) | None -> prerr_endline " _ ") l ; flush stderr ; +prerr_endline " + (* 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' = List.map (um_aux k) tl in + 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 k he with - C.Appl l -> C.Appl (l@tl') - | _ as he' -> C.Appl (he'::tl') + 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 _ as t -> t - | C.Abst _ as t -> t - | C.MutInd _ as t -> t - | C.MutConstruct _ as t -> t + | C.Const _ + | C.Abst _ + | C.MutInd _ + | C.MutConstruct _ as t -> t,metasenv | 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) + 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, cookingsno, i, outty', t', pl'),metasenv''' | 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 + 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) + C.Fix (i, liftedfl),metasenv' | 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 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) + C.CoFix (i, liftedfl),metasenv' in - um_aux 0 t,!unwinded + let t',metasenv' = um_aux metasenv t in + t',metasenv',!unwinded ;; (* apply_subst_reducing subst (Some (mtr,reductions_no)) t *) @@ -265,33 +395,33 @@ let unwind subst unwinded t = let apply_subst_reducing subst meta_to_reduce t = let unwinded = ref subst in - let rec um_aux k = + let rec um_aux = let module C = Cic in let module S = CicSubstitution in function - C.Rel _ as t -> t + C.Rel _ | C.Var _ as t -> t - | C.Meta i as t -> + | C.Meta (i,l) as t -> (try - S.lift k (List.assoc i !unwinded) + S.lift_meta l (List.assoc i !unwinded) with Not_found -> - C.Meta i) + C.Meta (i,l)) | 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.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 k) tl in + let tl' = List.map um_aux tl in let t' = - match um_aux k he with + match um_aux 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 -> + 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 -> @@ -303,7 +433,7 @@ let apply_subst_reducing subst meta_to_reduce t = | (_,t) -> t in beta_reduce (reductions_no,t') - | _ -> t' + | _,_ -> t' end | C.Appl _ -> assert false | C.Const _ as t -> t @@ -311,13 +441,13 @@ let apply_subst_reducing subst meta_to_reduce 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.MutCase (sp, cookingsno, 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 k ty, um_aux (k+len) bo)) + (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl in C.Fix (i, liftedfl) @@ -325,32 +455,60 @@ let apply_subst_reducing subst meta_to_reduce t = let len = List.length fl in let liftedfl = List.map - (fun (name, ty, bo) -> (name, um_aux k ty, um_aux (k+len) bo)) + (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl in C.CoFix (i, liftedfl) in - um_aux 0 t + um_aux t ;; (* UNWIND THE MGU INSIDE THE MGU *) -let unwind_subst subst = +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 (i,_) -> snd (unwind subst unwinded (Cic.Meta i))) [] subst + (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 = - fst (unwind [] 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. - 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. *) +(* 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 = - let subst_to_unwind = fo_unif_new metasenv context t1 t2 in - unwind_subst subst_to_unwind +prerr_endline "INIZIO FASE 1" ; flush stderr ; + let subst_to_unwind,metasenv' = fo_unif_new metasenv context 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 ;;