From: Claudio Sacerdoti Coen Date: Tue, 29 Oct 2002 13:56:26 +0000 (+0000) Subject: Bugs fixed: unification were not really explicit-named-substitutions aware. X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=474d5d18dc72061c923976ec9bf7a7f6ef828af3;p=helm.git Bugs fixed: unification were not really explicit-named-substitutions aware. It just compiled. --- diff --git a/helm/ocaml/cic_unification/cicUnification.ml b/helm/ocaml/cic_unification/cicUnification.ml index 66c88e60f..612931ed4 100644 --- a/helm/ocaml/cic_unification/cicUnification.ml +++ b/helm/ocaml/cic_unification/cicUnification.ml @@ -79,7 +79,11 @@ let delift context metasenv l t = ignore (deliftaux k (S.lift m t)) ; C.Rel ((position (m-k) l) + k) | None -> raise RelToHiddenHypothesis) - | C.Var _ as t -> t + | 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 @@ -194,6 +198,26 @@ let rec fo_unif_subst subst context metasenv t1 t2 = 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 _, _) @@ -264,6 +288,21 @@ let rec fo_unif_subst subst context metasenv t1 t2 = else raise UnificationFailed | (_,_) -> 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: ??????????????? @@ -399,9 +438,6 @@ let unwind metasenv subst unwinded t = 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 "