X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=8a1f4c43e8aef1d5fd25feb63f3a92c2ce829dcf;hb=fb0f22004d533abca8d157ed89665dbf1041e0e2;hp=35eb18f450974d61fc238b77d3f985203b249d6b;hpb=bc2a1fce21a66af077172344854c709b64b7fe82;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 35eb18f45..8a1f4c43e 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -43,6 +43,134 @@ let type_of_aux' metasenv subst context term = (CicMetaSubst.ppcontext subst context) (CicMetaSubst.ppmetasenv metasenv subst) msg))) +let rec eta_expand test_equality_only metasenv subst context t arg = + let module T = CicTypeChecker in + 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 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) as t-> + (try + let t' = List.assoc i subst in + aux metasenv subst n context t' + with + Not_found -> subst,metasenv,t) + | 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' + | 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' + + 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 = + T.type_of_aux' metasenv 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 + subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg] + +and eta_expand_many test_equality_only metasenv subst context t = + List.fold_left + (fun (subst,metasenv,t) arg -> + eta_expand test_equality_only metasenv subst context t arg + ) (subst,metasenv,t) + (* NUOVA UNIFICAZIONE *) (* A substitution is a (int * Cic.term) list that associates a metavariable i with its body. @@ -52,7 +180,7 @@ let type_of_aux' metasenv subst context term = a new substitution which is _NOT_ unwinded. It must be unwinded before applying it. *) -let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 = +and fo_unif_subst test_equality_only subst context metasenv t1 t2 = let module C = Cic in let module R = CicMetaSubst in let module S = CicSubstitution in @@ -203,25 +331,48 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; fo_unif_subst test_equality_only subst context metasenv t2 (S.subst s1 t1) | (C.Appl l1, C.Appl l2) -> - let lr1 = List.rev l1 in - let lr2 = List.rev l2 in - let rec fo_unif_l test_equality_only subst metasenv = - function - [],_ - | _,[] -> assert false - | ([h1],[h2]) -> - fo_unif_subst test_equality_only subst context metasenv h1 h2 - | ([h],l) - | (l,[h]) -> - fo_unif_subst - test_equality_only subst context metasenv h (C.Appl (List.rev l)) - | ((h1::l1),(h2::l2)) -> - let subst', metasenv' = - fo_unif_subst test_equality_only subst context metasenv h1 h2 - in - fo_unif_l test_equality_only subst' metasenv' (l1,l2) + let subst,metasenv,t1',t2' = + match l1,l2 with + (* In the first two cases when we reach the next begin ... end + section useless work is done since, by construction, the list + of arguments will be equal. + *) + C.Meta (i,l)::args, _ -> + let subst,metasenv,t2' = + eta_expand_many test_equality_only metasenv subst context t2 args + in + subst,metasenv,t1,t2' + | _, C.Meta (i,l)::args -> + let subst,metasenv,t1' = + eta_expand_many test_equality_only metasenv subst context t1 args + in + subst,metasenv,t1',t2 + | _,_ -> subst,metasenv,t1,t2 in - fo_unif_l test_equality_only subst metasenv (lr1, lr2) + begin + match t1',t2' with + C.Appl l1, C.Appl l2 -> + let lr1 = List.rev l1 in + let lr2 = List.rev l2 in + let rec fo_unif_l test_equality_only subst metasenv = + function + [],_ + | _,[] -> assert false + | ([h1],[h2]) -> + fo_unif_subst test_equality_only subst context metasenv h1 h2 + | ([h],l) + | (l,[h]) -> + fo_unif_subst + test_equality_only subst context metasenv h (C.Appl (List.rev l)) + | ((h1::l1),(h2::l2)) -> + let subst', metasenv' = + fo_unif_subst test_equality_only subst context metasenv h1 h2 + in + fo_unif_l test_equality_only subst' metasenv' (l1,l2) + in + fo_unif_l test_equality_only subst metasenv (lr1, lr2) + | _ -> assert false + end | (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