X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicUnification.ml;h=81e794c8c6f6709c873f6a6b49802b234ec6d7dc;hb=9945374a5594c068883fa6c775f17b640fcac64d;hp=8a1f4c43e8aef1d5fd25feb63f3a92c2ce829dcf;hpb=fb0f22004d533abca8d157ed89665dbf1041e0e2;p=helm.git diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 8a1f4c43e..81e794c8c 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -43,11 +43,11 @@ 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 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' = +(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*) try let subst,metasenv = fo_unif_subst test_equality_only subst context metasenv arg t' @@ -156,7 +156,7 @@ let rec eta_expand test_equality_only metasenv subst context t arg = subst,metasenv,(uri,t')::l) ens (subst,metasenv,[]) in let argty = - T.type_of_aux' metasenv context arg + type_of_aux' metasenv subst context arg in let fresh_name = FreshNamesGenerator.mk_fresh_name @@ -165,10 +165,10 @@ let rec eta_expand test_equality_only metasenv subst context t arg = 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 = +and beta_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 + beta_expand test_equality_only metasenv subst context t arg ) (subst,metasenv,t) (* NUOVA UNIFICAZIONE *) @@ -204,7 +204,7 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = (try let subst,metasenv = fo_unif_subst - test_equality_only subst context metasenv t1' t2' + test_equality_only subst context metasenv t1' t2' in true,subst,metasenv with @@ -236,53 +236,64 @@ and fo_unif_subst test_equality_only subst context metasenv t1 t2 = 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) + (lower m1 m2) (upper m1 m2) in - let subst'',metasenv' = + begin try let oldt = (List.assoc 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 + test_equality_only subst context metasenv t lifted_oldt with Not_found -> - 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 - (n, t'')::subst', metasenv' - in - 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 AssertFailure _ -> - (* 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) - *) + (* First of all we unify the type of the meta with the type of the term *) + 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 AssertFailure _ -> + (* 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) + *) (* prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN."; prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; *) - (subst'', metasenv')) + (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 = (List.assoc 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 + Not_found -> + (n,t'')::subst, metasenv + end | (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 @@ -333,21 +344,24 @@ prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ; | (C.Appl l1, C.Appl l2) -> let subst,metasenv,t1',t2' = match l1,l2 with + C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j -> + subst,metasenv,t1,t2 (* 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, _ -> + | C.Meta (i,l)::args, _ -> let subst,metasenv,t2' = - eta_expand_many test_equality_only metasenv subst context t2 args + beta_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 + beta_expand_many test_equality_only metasenv subst context t1 args in subst,metasenv,t1',t2 - | _,_ -> subst,metasenv,t1,t2 + | _,_ -> + subst,metasenv,t1,t2 in begin match t1',t2' with