X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=d3c86d2816c2c9bd050bbe1b336d033d95e4c8dd;hb=1ee5193677b8e2a80d4f068ee79ecac335de1196;hp=11f90736a23e01ff088d54779c574c7d8dc679f6;hpb=e8fb6062a3c126dc242ee7bc44a696d73ca8ed76;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 11f90736a..d3c86d281 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -68,6 +68,28 @@ let eta_reduce = module C = NCic;; module Ref = NReference;; +let indent = ref "";; +let inside c = indent := !indent ^ String.make 1 c;; +let outside () = indent := String.sub !indent 0 (String.length !indent -1);; + +let pp s = + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; + +(* let pp _ = ();; *) + +let fix_sorts metasenv subst context meta t = + let rec aux () = function + | NCic.Sort (NCic.Type u) as orig -> + (match NCicEnvironment.sup u with + | None -> raise (fail_exc metasenv subst context meta t) + | Some u1 -> if u = u1 then orig else NCic.Sort (NCic.Type u1)) + | NCic.Meta _ as orig -> orig + | t -> NCicUtils.map (fun _ _ -> ()) () aux t + in + aux () t +;; + let rec beta_expand 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 @@ -111,6 +133,10 @@ let rec beta_expand num test_eq_only swap metasenv subst context t arg = metasenv, subst, NCic.Lambda ("_", argty, NCicSubstitution.lift 1 arg) and beta_expand_many 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) -> @@ -120,46 +146,81 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = 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 *) and instantiate test_eq_only metasenv subst context n lc t swap = + (*D*) inside 'I'; try let rc = let unify test_eq_only m s c t1 t2 = if swap then unify test_eq_only m s c t2 t1 else unify test_eq_only m s c t1 t2 in - let ty_t = - try NCicTypeChecker.typeof ~subst ~metasenv context t - with NCicTypeChecker.TypeCheckerFailure msg -> - prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t); - prerr_endline (Lazy.force msg); - assert false + let fix_sorts t = + if swap then fix_sorts metasenv subst context (NCic.Meta (n,lc)) t + else + NCic.Sort (NCic.Type ( + match NCicEnvironment.sup NCicEnvironment.type0 with Some x ->x| _ -> + assert false)) in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in - let lty = NCicSubstitution.subst_meta lc ty in - let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in + let metasenv, subst, t = + match ty with + | NCic.Implicit (`Typeof _) -> metasenv, subst, fix_sorts t + | _ -> + pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t)); + let t, ty_t = + try t, NCicTypeChecker.typeof ~subst ~metasenv context t + with NCicTypeChecker.TypeCheckerFailure _ -> + let ft = fix_sorts t in + if ft == t then assert false else + try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + ft, NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.TypeCheckerFailure msg -> + prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context ft); + prerr_endline (Lazy.force msg); + assert false + in + let lty = NCicSubstitution.subst_meta lc ty in + pp (lazy("On the types: " ^ + NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " + ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t)); + let metasenv,subst= unify test_eq_only metasenv subst context lty ty_t in + metasenv, subst, t + in let (metasenv, subst), t = - NCicMetaSubst.delift metasenv subst context n lc t + try NCicMetaSubst.delift metasenv subst context n lc t + with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg) + | NCicMetaSubst.MetaSubstFailure msg -> raise (UnificationFailure msg) in (* Unifying the types may have already instantiated n. *) try let _, _,oldt,_ = NCicUtils.lookup_subst n subst in let oldt = NCicSubstitution.subst_meta lc oldt in + let t = NCicSubstitution.subst_meta lc t in (* conjecture: always fail --> occur check *) unify test_eq_only metasenv subst context oldt t with NCicUtils.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 + pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm + ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t))); let metasenv = List.filter (fun (m,_) -> not (n = m)) metasenv in metasenv, subst + (*D*) in outside(); rc with exn -> outside (); raise exn and unify test_eq_only metasenv subst context t1 t2 = + (*D*) inside 'U'; try let rc = let fo_unif test_eq_only metasenv subst t1 t2 = - prerr_endline ("A " ^ - NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ NCicPp.ppterm - ~metasenv ~subst ~context t2 ); + (*D*) inside 'F'; try let rc = + pp (lazy(" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2)); if t1 === t2 then metasenv, subst else @@ -343,32 +404,44 @@ and unify test_eq_only metasenv subst context t1 t2 = raise (uncert_exc metasenv subst context t1 t2)) | (C.Implicit _, _) | (_, C.Implicit _) -> assert false | _ -> raise (uncert_exc metasenv subst context t1 t2) + (*D*) in outside(); rc with exn -> outside (); raise exn in - let height_of is_whd = function + let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) | NCic.Const (Ref.Ref (_,Ref.Fix (_,_,h))) | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Def h))::_) - | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h, false - | NCic.Meta _ | NCic.Appl (NCic.Meta _ :: _) -> max_int, true -(* | NCic.Rel _ -> 1, WRONG *) - | _ when is_whd -> 0, false - | _ -> max_int, false + | NCic.Appl(NCic.Const(Ref.Ref(_,Ref.Fix (_,_,h)))::_) -> h + | _ -> 0 + in + let put_in_whd m1 m2 = + NCicReduction.reduce_machine ~delta:max_int ~subst context m1, + NCicReduction.reduce_machine ~delta:max_int ~subst context m2 in - let small_delta_step is_whd (_,_,t1,_ as m1) (_,_,t2,_ as m2) = - let h1, flex1 = height_of is_whd t1 in - let h2, flex2 = height_of is_whd t2 in + let small_delta_step + ((_,_,t1,_ as m1, norm1) as x1) ((_,_,t2,_ as m2, norm2) as x2) + = + assert (not (norm1 && norm2)); + if norm1 then + x1,NCicReduction.reduce_machine ~delta:(height_of t2 -1) ~subst context m2 + else if norm2 then + NCicReduction.reduce_machine ~delta:(height_of t1 -1) ~subst context m1,x2 + else + let h1 = height_of t1 in + let h2 = height_of t2 in let delta = if h1 = h2 then max 0 (h1 -1) else min h1 h2 in NCicReduction.reduce_machine ~delta ~subst context m1, - NCicReduction.reduce_machine ~delta ~subst context m2, - if is_whd && flex1 && flex2 then 0 else delta + NCicReduction.reduce_machine ~delta ~subst context m2 in - let rec unif_machines metasenv subst = function - | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) -> - prerr_endline ("M(" ^ string_of_int delta^ " " ^ - NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ - " === " ^ NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind - m2)); - try + let rec unif_machines metasenv subst = + function + | ((k1,e1,t1,s1),norm1 as m1),((k2,e2,t2,s2),norm2 as m2) -> + (*D*) inside 'M'; try let rc = +(* + pp (lazy((if are_normal then "*" else " ") ^ " " ^ + NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^ + " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); +*) let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r @@ -377,8 +450,7 @@ and unify test_eq_only metasenv subst context t1 t2 = try let t1 = NCicReduction.from_stack t1 in let t2 = NCicReduction.from_stack t2 in - unif_machines metasenv subst - (small_delta_step true t1 t2) + unif_machines metasenv subst (put_in_whd t1 t2) with UnificationFailure _ | Uncertain _ when not b -> metasenv, subst in @@ -395,27 +467,25 @@ and unify test_eq_only metasenv subst context t1 t2 = (NCicReduction.unwind (k1,e1,t1,List.rev l1)) (NCicReduction.unwind (k2,e2,t2,List.rev l2)) in - check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) - with UnificationFailure _ | Uncertain _ when delta > 0 -> -(* - let delta = delta - 1 in - let red = NCicReduction.reduce_machine ~delta ~subst context in -*) - prerr_endline ("RIPARTO RIDUCENDO"^string_of_int delta); - unif_machines metasenv subst (small_delta_step true m1 m2) - | exn -> prerr_endline ")"; raise exn + try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) + with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> + unif_machines metasenv subst (small_delta_step m1 m2) + (*D*) in outside(); rc with exn -> outside (); raise exn in try fo_unif test_eq_only metasenv subst t1 t2 with UnificationFailure msg | Uncertain msg as exn -> try unif_machines metasenv subst - (small_delta_step false (0,[],t1,[]) (0,[],t2,[])) + (put_in_whd (0,[],t1,[]) (0,[],t2,[])) with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn + (*D*) in outside(); rc with exn -> outside (); raise exn ;; -let unify = unify false;; +let unify = + indent := ""; + unify false;;