From: Enrico Tassi Date: Mon, 6 Apr 2009 09:01:59 +0000 (+0000) Subject: snapshot X-Git-Tag: make_still_working~4120 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d7f32114f3806b51c2ee483dcb5a86e08d086a72;p=helm.git snapshot --- diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml index 3f2f43df0..5062353cd 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.ml +++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml @@ -196,8 +196,25 @@ and restrict metasenv subst i restrictions = (* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), otherwise the occur check does not make sense in case of unification of ?n with ?n *) -let delift metasenv subst context n l t = - let rec aux k (metasenv, subst as ms) = function +let delift ~unify metasenv subst context n l t = + let unify_list = + match l with + | _, NCic.Irl _ -> fun _ _ _ _ _ -> None + | shift, NCic.Ctx l -> fun metasenv subst context k t -> + HExtlib.list_findopt + (fun li i -> + let li = NCicSubstitution.lift (k+shift) li in + match unify metasenv subst context li t with + | Some (metasenv,subst) -> + Some ((metasenv, subst), NCic.Rel (i+1+k)) + | None -> None) + l + in + let rec aux k (metasenv, subst as ms) t = + match unify_list metasenv subst context k t with + | Some x -> x + | None -> + match t with | NCic.Rel n as t when n <= k -> ms, t | NCic.Rel n -> (try @@ -219,7 +236,8 @@ let delift metasenv subst context n l t = (NCicPp.ppterm ~context ~metasenv ~subst t)))) | NCic.Meta (i,l1) as orig -> (try - let _,_,t,_ = NCicUtils.lookup_subst i subst in + let tag,_,t,_ = NCicUtils.lookup_subst i subst in + (match tag with None -> () | Some tag -> prerr_endline tag); aux k ms (NCicSubstitution.subst_meta l1 t) with NCicUtils.Subst_not_found _ -> if snd l1 = NCic.Irl 0 || snd l1 = NCic.Ctx [] then ms, orig diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.mli b/helm/software/components/ng_refiner/nCicMetaSubst.mli index 033ea1b1b..293e3a01f 100644 --- a/helm/software/components/ng_refiner/nCicMetaSubst.mli +++ b/helm/software/components/ng_refiner/nCicMetaSubst.mli @@ -43,6 +43,8 @@ val restrict : * in the term (for occur check). *) val delift : + unify:(NCic.metasenv -> NCic.substitution -> NCic.context -> + NCic.term -> NCic.term -> (NCic.metasenv * NCic.substitution) option) -> NCic.metasenv -> NCic.substitution -> NCic.context -> int -> NCic.local_context -> NCic.term -> (NCic.metasenv * NCic.substitution) * NCic.term diff --git a/helm/software/components/ng_refiner/nCicRefiner.ml b/helm/software/components/ng_refiner/nCicRefiner.ml index 7871d86e9..8c5dcae76 100644 --- a/helm/software/components/ng_refiner/nCicRefiner.ml +++ b/helm/software/components/ng_refiner/nCicRefiner.ml @@ -309,7 +309,7 @@ let rec typeof hdb let resty = C.Appl (outtype::arguments@[term]) in let resty = NCicReduction.head_beta_reduce ~subst resty in metasenv, subst, C.Match (r, outtype, term, List.rev pl_rev),resty - | C.Match _ as orig -> assert false + | C.Match _ -> assert false in pp (lazy (NCicPp.ppterm ~metasenv ~subst ~context t ^ " :: "^ NCicPp.ppterm ~metasenv ~subst ~context infty )); @@ -586,7 +586,7 @@ let typeof_obj hdb uri, height, metasenv, subst, C.Fixpoint (inductive, fl, attr) - | C.Inductive (ind, leftno, itl, attr) -> assert false + | C.Inductive (_ind, _leftno, _itl, _attr) -> assert false (* (* let's check if the arity of the inductive types are well formed *) List.iter (fun (_,_,x,_) -> ignore (typeof ~subst ~metasenv [] x)) tyl; diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 55ccca12a..f23116b63 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -98,66 +98,21 @@ let fix_sorts swap metasenv subst context meta t = aux () t ;; -let rec beta_expand hdb num test_eq_only swap metasenv subst context t arg = - let rec aux (n,context,test_eq_only as k) (metasenv, subst as acc) t' = - try - let metasenv, subst = - if swap then - unify hdb test_eq_only metasenv subst context t' (NCicSubstitution.lift n arg) - else - unify hdb test_eq_only metasenv subst context (NCicSubstitution.lift n arg) t' - in - (metasenv, subst), NCic.Rel (1 + n) - with Uncertain _ | UnificationFailure _ -> - match t' with - | NCic.Rel m as orig -> - (metasenv, subst), if m <= n then orig else NCic.Rel (m+1) - (* 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 *) - | NCic.Meta (i,(shift,lc)) -> - (metasenv,subst), NCic.Meta (i,(shift+1,lc)) - | NCic.Prod (name, src, tgt) as orig -> - let (metasenv, subst), src1 = aux (n,context,true) acc src in - let k = n+1, (name, NCic.Decl src) :: context, test_eq_only in - let ms, tgt1 = aux k (metasenv, subst) tgt in - if src == src1 && tgt == tgt1 then ms, orig else - ms, NCic.Prod (name, src1, tgt1) - | t -> - NCicUntrusted.map_term_fold_a - (fun e (n,ctx,teq) -> n+1,e::ctx,teq) k aux acc t - - in - let argty = NCicTypeChecker.typeof ~metasenv ~subst context arg in - let fresh_name = "Hbeta" ^ string_of_int num in - let (metasenv,subst), t1 = - aux (0, context, test_eq_only) (metasenv, subst) t in - let t2 = eta_reduce (NCic.Lambda (fresh_name,argty,t1)) in - try - ignore(NCicTypeChecker.typeof ~metasenv ~subst context t2); - metasenv, subst, t2 - with NCicTypeChecker.TypeCheckerFailure _ -> - metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) - -and beta_expand_many hdb test_equality_only swap metasenv subst context t args = -(* (*D*) inside 'B'; try let rc = *) - pp (lazy (String.concat ", " - (List.map (NCicPp.ppterm ~metasenv ~subst ~context) - args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); - let _, subst, metasenv, hd = - List.fold_right - (fun arg (num,subst,metasenv,t) -> - let metasenv, subst, t = - beta_expand hdb num test_equality_only swap metasenv subst context t arg - in - num+1,subst,metasenv,t) - args (1,subst,metasenv,t) - in - pp (lazy ("Head syntesized by b-exp: " ^ - NCicPp.ppterm ~metasenv ~subst ~context hd)); - metasenv, subst, hd -(* (*D*) in outside (); rc with exn -> outside (); raise exn *) +let rec beta_expand_many metasenv subst context t args = + let tty = NCicTypeChecker.typeof ~metasenv ~subst context t in + let argsty = List.map (NCicTypeChecker.typeof ~metasenv ~subst context) args in + let rec mk_lambda context n = function + | [] -> + let metasenv, _, bo, _ = + NCicMetaSubst.mk_meta metasenv context (`WithType tty) in + metasenv, bo + | ty::tail -> + let name = "HBeta"^string_of_int n in + let ty = NCicSubstitution.lift n ty in + let metasenv, bo = mk_lambda ((name,NCic.Decl ty)::context) (n+1) tail in + metasenv, NCic.Lambda (name, ty, bo) + in + mk_lambda context 0 argsty and instantiate hdb test_eq_only metasenv subst context n lc t swap = (*D*) inside 'I'; try let rc = @@ -214,7 +169,16 @@ and instantiate hdb test_eq_only metasenv subst context n lc t swap = pp (lazy(string_of_int n ^ " := 111 = "^ NCicPp.ppterm ~metasenv ~subst ~context t)); let (metasenv, subst), t = - try NCicMetaSubst.delift metasenv subst context n lc t + try + NCicMetaSubst.delift + ~unify:(fun m s c t1 t2 -> + let ind = !indent in + let res = + try Some (unify test_eq_only m s c t1 t2 ) + with UnificationFailure _ | Uncertain _ -> None + in + indent := ind; res) + metasenv subst context n lc t with NCicMetaSubst.Uncertain msg -> pp (lazy ("delift fails: " ^ Lazy.force msg)); raise (Uncertain msg) @@ -355,22 +319,26 @@ and unify hdb test_eq_only metasenv subst context t1 t2 = | 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 metasenv, subst, beta_expanded = - beta_expand_many hdb - test_eq_only false - metasenv subst context t2 args + let metasenv, beta_expanded = + beta_expand_many metasenv subst context t2 args in + let metasenv, subst = unify hdb test_eq_only metasenv subst context - (C.Meta (i,l)) beta_expanded + (C.Meta (i,l)) beta_expanded + in + + (* .... eta_reduce ?i ... *) + unify hdb test_eq_only metasenv subst context t1 t2 | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) -> - let metasenv, subst, beta_expanded = - beta_expand_many hdb - test_eq_only true - metasenv subst context t1 args + let metasenv, beta_expanded = + beta_expand_many metasenv subst context t1 args in + let metasenv, subst = unify hdb test_eq_only metasenv subst context - beta_expanded (C.Meta (i,l)) + beta_expanded (C.Meta (i,l)) + in + unify hdb test_eq_only metasenv subst context t1 t2 (* processing this case here we avoid a useless small delta step *) | (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))