X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=306074ec983daf7b0adda12e594efb0bb5f7222a;hb=60c7321771851b82493bb202185ee184f1e7a3d1;hp=4a2cb243066b0a1b3efb0be2a7f88a54aaee65b4;hpb=0328c0e2938ce714d5d7358afdca00195577198e;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 4a2cb2430..306074ec9 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -49,14 +49,14 @@ let position n = 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) + [] -> [] + | _::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 + [] -> [] + | (n,context,t)::tl -> (n,erase 1 n context,t)::(aux tl) in aux ;; @@ -72,14 +72,18 @@ let delift context metasenv l t = 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) -> + (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 _ as t -> t + | 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 @@ -103,12 +107,23 @@ let delift context metasenv l 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, + | 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 @@ -145,115 +160,154 @@ type substitution = (int * Cic.term) list 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 context metasenv t1 t2 = - 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_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 _, _) - | (_, 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_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 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 _, _) - | (_, C.Abst _) - | (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_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, metasenv - else raise UnificationFailed - | (_,_) -> raise UnificationFailed - in fo_unif_aux [] context metasenv t1 t2;; +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 @@ -268,24 +322,24 @@ 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 + [] -> [] + | 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) + [] -> [] + | (n,context,t)::tl when n=m -> (n,erase 1 context,t)::tl + | hd::tl -> hd::(aux tl) in aux ;; @@ -324,40 +378,39 @@ CSCSCS | C.Sort _ -> metasenv | C.Implicit -> metasenv | C.Cast (te,ty) -> - let metasenv' = aux metasenv k te in - aux metasenv' k 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 + 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 + 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 + 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 + 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 + 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 + let (_,ty,bo) = f in + let metasenv' = aux metasenv k ty in + aux metasenv' (k+len) bo ) metasenv fl in aux metasenv 0 ;; @@ -374,24 +427,21 @@ let unwind metasenv subst unwinded t = C.Rel _ as t -> t,metasenv | C.Var _ as t -> t,metasenv | C.Meta (i,l) -> - (try + (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 ; + frozen := i::!frozen ; let res = try - let t = List.assoc i subst in + let t = List.assoc i subst in let t',metasenv' = um_aux metasenv t in - let _,metasenv'' = + 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 " + (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) + let t',metasenv' = um_aux metasenv t in + (Some t')::tl, metasenv' + ) l ([],metasenv) in C.Meta (i,l'), metasenv' in @@ -435,10 +485,10 @@ prerr_endline " let tl',metasenv' = List.fold_right - (fun t (tl,metasenv) -> - let t',metasenv' = um_aux metasenv t in - t'::tl, metasenv' - ) tl ([],metasenv) + (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 @@ -446,30 +496,53 @@ prerr_endline " C.Appl (he'::tl'),metasenv'' end | C.Appl _ -> assert false - | C.Const _ - | C.Abst _ - | C.MutInd _ - | C.MutConstruct _ as t -> t,metasenv - | C.MutCase (sp,cookingsno,i,outty,t,pl) -> + | 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'') + (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.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) + 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) -> @@ -477,10 +550,10 @@ prerr_endline " - let ty',metasenv' = um_aux metasenv ty in - let bo',metasenv'' = um_aux metasenv' bo in - (name, ty', bo')::fl,metasenv'' - ) 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 @@ -541,12 +614,23 @@ let apply_subst_reducing subst meta_to_reduce 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 outty, um_aux t, + | 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 @@ -610,7 +694,7 @@ let apply_subst subst t = (* 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_new metasenv context t1 t2 in + 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