From: Enrico Tassi Date: Thu, 25 Sep 2008 11:44:40 +0000 (+0000) Subject: ... X-Git-Tag: make_still_working~4742 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fdd518320bc83f20e8cef9dd6638c9cf6dd6345d;p=helm.git ... --- diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 6a4781794..29851b5d4 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -23,7 +23,251 @@ let fail_exc metasenv subst context t1 t2 = " with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2)) ;; -let unify metasenv subst context t1 t2 = +let mk_appl hd tl = + match hd with + | NCic.Appl l -> NCic.Appl (l@tl) + | _ -> NCic.Appl (hd :: tl) +;; + +let flexible l = + List.exists + (function + | NCic.Meta _ + | NCic.Appl (NCic.Meta _::_) -> true + | _ -> false) l +;; + +exception WrongShape;; + +let eta_reduce after_beta_expansion after_beta_expansion_body + before_beta_expansion + = + try + match before_beta_expansion,after_beta_expansion_body with + Cic.Appl l, Cic.Appl l' -> + let rec all_but_last check_last = + function + [] -> assert false + | [Cic.Rel 1] -> [] + | [_] -> if check_last then raise WrongShape else [] + | he::tl -> he::(all_but_last check_last tl) + in + let all_but_last check_last l = + match all_but_last check_last l with + [] -> assert false + | [he] -> he + | l -> Cic.Appl l + in + let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in + let all_but_last = all_but_last false l in + (* here we should test alpha-equivalence; however we know by + construction that here alpha_equivalence is equivalent to = *) + if t = all_but_last then + all_but_last + else + after_beta_expansion + | _,_ -> after_beta_expansion + with + WrongShape -> after_beta_expansion + +let rec beta_expand num test_equality_only metasenv subst context t arg ugraph = + let module S = CicSubstitution in + let module C = Cic in +let foo () = + let rec aux metasenv subst n context t' ugraph = + try + + let subst,metasenv,ugraph1 = + fo_unif_subst test_equality_only subst context metasenv + (CicSubstitution.lift n arg) t' ugraph + + in + subst,metasenv,C.Rel (1 + n),ugraph1 + with + Uncertain _ + | UnificationFailure _ -> + match t' with + | C.Rel m -> subst,metasenv, + (if m <= n then C.Rel m else C.Rel (m+1)),ugraph + | C.Var (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1 + | C.Meta (i,l) -> + (* andrea: in general, beta_expand can create badly typed + terms. This happens quite seldom in practice, UNLESS we + iterate on the local context. For this reason, we renounce + to iterate and just lift *) + let l = + List.map + (function + Some t -> Some (CicSubstitution.lift 1 t) + | None -> None) l in + subst, metasenv, C.Meta (i,l), ugraph + | C.Sort _ + | C.Implicit _ as t -> subst,metasenv,t,ugraph + | C.Cast (te,ty) -> + let subst,metasenv,te',ugraph1 = + aux metasenv subst n context te ugraph in + let subst,metasenv,ty',ugraph2 = + aux metasenv subst n context ty ugraph1 in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Cast (te', ty')),ugraph2 + | C.Prod (nn,s,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t + ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Prod (nn, s', t')),ugraph2 + | C.Lambda (nn,s,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.Lambda (nn, s', t')),ugraph2 + | C.LetIn (nn,s,ty,t) -> + let subst,metasenv,s',ugraph1 = + aux metasenv subst n context s ugraph in + let subst,metasenv,ty',ugraph1 = + aux metasenv subst n context ty ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t + ugraph1 + in + (* TASSI: sure this is in serial? *) + subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2 + | C.Appl l -> + let subst,metasenv,revl',ugraph1 = + List.fold_left + (fun (subst,metasenv,appl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::appl),ugraph1 + ) (subst,metasenv,[],ugraph) l + in + subst,metasenv,(C.Appl (List.rev revl')),ugraph1 + | C.Const (uri,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1 + | C.MutInd (uri,i,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1 + | C.MutConstruct (uri,i,j,exp_named_subst) -> + let subst,metasenv,exp_named_subst',ugraph1 = + aux_exp_named_subst metasenv subst n context exp_named_subst ugraph + in + subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1 + | C.MutCase (sp,i,outt,t,pl) -> + let subst,metasenv,outt',ugraph1 = + aux metasenv subst n context outt ugraph in + let subst,metasenv,t',ugraph2 = + aux metasenv subst n context t ugraph1 in + let subst,metasenv,revpl',ugraph3 = + List.fold_left + (fun (subst,metasenv,pl,ugraph) t -> + let subst,metasenv,t',ugraph1 = + aux metasenv subst n context t ugraph in + subst,metasenv,(t'::pl),ugraph1 + ) (subst,metasenv,[],ugraph2) pl + in + subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3 + (* TASSI: not sure this is serial *) + | 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,(CicSubstitution.lift 1 t' ),ugraph + | 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,(CicSubstitution.lift 1 t'), ugraph + + and aux_exp_named_subst metasenv subst n context ens ugraph = + List.fold_right + (fun (uri,t) (subst,metasenv,l,ugraph) -> + let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in + subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph) + in + let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in + let fresh_name = + FreshNamesGenerator.mk_fresh_name ~subst + metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty + in + let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in + let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in + subst, metasenv, t'', ugraph2 +in profiler_beta_expand.HExtlib.profile foo () + + +and beta_expand_many test_equality_only metasenv subst context t args ugraph = + let _,subst,metasenv,hd,ugraph = + List.fold_right + (fun arg (num,subst,metasenv,t,ugraph) -> + let subst,metasenv,t,ugraph1 = + beta_expand num test_equality_only + metasenv subst context t arg ugraph + in + num+1,subst,metasenv,t,ugraph1 + ) args (1,subst,metasenv,t,ugraph) + in + subst,metasenv,hd,ugraph + + + +let rec instantiate test_eq_only metasenv subst context n lc t swap = + let unif m s c t1 t2 = + if swap then unify m s c t2 t1 else unify m s c t1 t2 + in + let ty_t = + try NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure _ -> assert false + in + let name, ctx, ty = NCicUtils.lookup_meta n metasenv in + let ty = NCicSubstitution.subst_meta lc ty in + let metasenv, subst = unify metasenv susbt context ty ty_t in + let (metasenv, subst), t = + NCicMetaSubst.delift metasenv subst context n lc t + in + (* Unifying the types may have already instantiated n. *) + try + let _, _,oldt,_ = CicUtil.lookup_subst n subst in + let oldt = NCicSubstitution.subst_meta lc oldt in + (* conjecture: always fail --> occur check *) + unify test_eq_only metasenv subst context oldt t + with CicUtil.Subst_not_found _ -> + (* by cumulativity when unify(?,Type_i) + * we could ? := Type_j with j <= i... *) + let subst = (n, (name, ctx, t, ty)) :: subst in + let metasenv = + List.filter (fun (m,_) -> not (n = m)) metasenv + in + subst, metasenv + +and unify metasenv subst context t1 t2 = let rec aux test_eq_only metasenv subst context t1 t2 = let fo_unif test_eq_only metasenv subst t1 t2 = if t1 === t2 then @@ -79,25 +323,61 @@ let unify metasenv subst context t1 t2 = aux test_eq_only metasenv subst context term1 term2 with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg)) - | C.Meta (n1,l1), _ - | _, C.Meta (n2,l2) -> + | C.Meta (n,lc), t -> + try + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + aux test_eq_only metasenv subst context term t + with NCicUtils.Subst_not_found _-> + instantiate test_eq_only metasenv subst context n lc t false + + | t, C.Meta (n,lc) -> + try + let _,_,term,_ = NCicUtils.lookup_subst n subst in + let term = NCicSubstitution.subst_meta lc term in + aux test_eq_only metasenv subst context t term + with NCicUtils.Subst_not_found _-> + instantiate test_eq_only metasenv subst context n lc t true + | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst -> + let _,_,term,_ = NCicUtils.lookup_subst i subst in + let term = NCicSubstitution.subst_meta l term in + aux test_eq_only metasenv subst context (mk_appl term args) t2 + | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst -> + let _,_,term,_ = NCicUtils.lookup_subst i subst in + let term = NCicSubstitution.subst_meta l term in + aux test_eq_only metasenv subst context t1 (mk_appl term args) + | NCic.Appl (NCic.Meta (i,_)::_ as l1), + NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j -> + try + List.fold_left2 + (fun (metasenv, subst) t1 t2 -> + aux test_eq_only metasenv subst context t1 t2) + (metasenv,subst) l1 l2 + with Invalid_argument _ -> + raise (fail_exc metasenv subst context t1 t2) - (try - let _,_,term,_ = NCicUtils.lookup_subst n1 subst in - let term = NCicSubstitution.subst_meta l1 term in - aux test_eq_only metasenv subst context term t2 - with NCicUtils.Subst_not_found _ -> - - ) - (try - let _,_,term,_ = NCicUtils.lookup_subst n2 subst in - let term = NCicSubstitution.subst_meta l2 term in - aux test_eq_only metasenv subst context t1 term - with NCicUtils.Subst_not_found _ -> false) - + | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) -> + (* we verify that none of the args is a Meta, + since beta expanding w.r.t a metavariable makes no sense *) + let subst, metasenv, beta_expanded = + beta_expand_many + test_equality_only metasenv subst context t2 args ugraph + in + aux test_eq_only metasenv subst context + (C.Meta (i,l)) beta_expanded + | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) -> + let subst,metasenv,beta_expanded = + beta_expand_many + test_equality_only + metasenv subst context t1 args ugraph + in + fo_unif_subst test_equality_only subst context metasenv + (C.Meta (i,l)) beta_expanded ugraph1 + | _,_ -> +....... | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2)) when (Ref.eq r1 r2 && List.length (E.get_relevance r1) >= List.length tl1) ->