From 68e7533f986352a86ea0288909b27f83d44893a6 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 6 Oct 2008 16:53:01 +0000 Subject: [PATCH] slow example --- helm/software/components/ng_refiner/check.ml | 1 - .../software/components/ng_refiner/esempio.ma | 37 ++++++++++- .../components/ng_refiner/nCicUnification.ml | 65 ++++++++++--------- 3 files changed, 69 insertions(+), 34 deletions(-) diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 1da400206..82aff623b 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -245,7 +245,6 @@ let _ = *) let metasenv, subst = try -(* prerr_endline ("INIZIO: " ^ NUri.string_of_uri u); *) NCicUnification.unify menv [] ctx left right with | NCicUnification.Uncertain msg diff --git a/helm/software/components/ng_refiner/esempio.ma b/helm/software/components/ng_refiner/esempio.ma index 613448a61..d0f6a2e86 100644 --- a/helm/software/components/ng_refiner/esempio.ma +++ b/helm/software/components/ng_refiner/esempio.ma @@ -15,15 +15,46 @@ include "nat/plus.ma". definition hole : ∀A:Type.A → A ≝ λA.λx.x. +definition id : ∀A:Type.A → A ≝ λA.λx.x. +(* meta1 Vs meta2 with different contexts axiom foo: ∀P:Type.∀f:P→P→Prop.∀x:P. (λw. ((∀e:P.f x (w x)) = (∀y:P. f x (hole ? y)))) - (λw:P.hole ? w). (* OK *) - + (λw:P.hole ? w). +*) + +(* meta1 Vs meta1 with different local contexts axiom foo: ∀P:Type.∀f:P→P→P.∀x,y:P. - (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w). (* OK, restringe Rel1 *) + (λw.(f x (w x) = f x (w y))) (λw:P.hole ? w). +*) + +(* meta Vs term && term Vs meta with different local ctx +axiom foo: + ∀P:Type.∀f:P→P→P.∀x,y:P. + (λw.(f (w x) (hole ? x) = f x (w y))) (λw:P.hole ? w). +*) + +(* occur check +axiom foo: + ∀P:Type.∀f:P→P→P.∀x,y:P. + (λw.(f x (f (w x) x) = f x (w y))) (λw:P.hole ? w). +*) + +(* unifying the type of (y ?) with (Q x) we instantiate ? to x +axiom foo: + ∀P:Type.∀Q:P→Type.∀f:∀x:P.Q x→P→P.∀x:P.∀y:∀x.Q x. + (λw.(f w (y w) x = (id ? f) x (hole ? (y x)) x)) (hole ? x). +*) + +alias num (instance 0) = "natural number". +axiom foo: (12+12) = (12+11). + + + (id ?(id ?(id ?(id ? (100+100))))) = + (id ?(id ?(id ?(id ? (99+100))))).[3: + apply (refl_eq nat (id ?(id ?(id ?(id ? (98+102+?)))))); axiom foo: (λx,y.(λz. z (x+y) + z x) (λw:nat.hole ? w)) = λx,y.x. (* OK *) axiom foo: (λx,y.(λz. z x + z (x+y)) (λw:nat.hole ? w)) = λx,y.x. (* KO, delift rels only *) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index d4a136597..a12ef1164 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -72,10 +72,13 @@ 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 ^ " " ^ s);; + prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) +;; +*) -(* let pp _ = ();; *) +let pp _ = ();; 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' = @@ -120,9 +123,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 (String.concat ", " (List.map (NCicPp.ppterm ~metasenv ~subst ~context) - args) ^ " ∈ " ^ NCicPp.ppterm ~metasenv ~subst ~context t); +(* (*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) -> @@ -132,13 +136,13 @@ 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 ("Head syntesized by b-exp: " ^ - NCicPp.ppterm ~metasenv ~subst ~context hd); + 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 +(* (*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 = +(* (*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 @@ -152,8 +156,9 @@ and instantiate test_eq_only metasenv subst context n lc t swap = in let name, ctx, ty = NCicUtils.lookup_meta n metasenv in let lty = NCicSubstitution.subst_meta lc ty in - pp ("On the types: " ^ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === " - ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t); + 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 let (metasenv, subst), t = try NCicMetaSubst.delift metasenv subst context n lc t @@ -170,20 +175,22 @@ and instantiate test_eq_only metasenv subst context n lc t swap = (* by cumulativity when unify(?,Type_i) * we could ? := Type_j with j <= i... *) let subst = (n, (name, ctx, t, ty)) :: subst in - pp ("?"^string_of_int n^" := "^NCicPp.ppterm - ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)); + pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm + ~metasenv ~subst ~context:ctx (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 +(* (*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 = +(* (*D*) inside 'U'; try let rc = *) let fo_unif test_eq_only metasenv subst t1 t2 = - (*D*) inside 'F'; try let rc = - pp (" " ^ 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 @@ -367,7 +374,7 @@ 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 +(* (*D*) in outside(); rc with exn -> outside (); raise exn *) in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) @@ -389,7 +396,7 @@ and unify test_eq_only metasenv subst context t1 t2 = if flexible [t2] then max 0 (h1 - 1) else if h1 = h2 then max 0 (h1 -1) else min h1 h2 in - pp ("DELTA STEP TO: " ^ string_of_int delta); + pp (lazy("DELTA STEP TO: " ^ string_of_int delta)); let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in if (m1' == m1 && m2' == m2 && delta > 0) then @@ -398,7 +405,7 @@ and unify test_eq_only metasenv subst context t1 t2 = * rec argument. if no reduction was performed we decrease delta to m-1 * to reduce the other term *) let delta = delta - 1 in - pp ("DELTA STEP TO: " ^ string_of_int delta); + pp (lazy("DELTA STEP TO: " ^ string_of_int delta)); let m1' = NCicReduction.reduce_machine ~delta ~subst context m1 in let m2' = NCicReduction.reduce_machine ~delta ~subst context m2 in m1', m2', (m1 == m1' && m2 == m2') || delta = 0 @@ -407,11 +414,13 @@ and unify test_eq_only metasenv subst context t1 t2 = let rec unif_machines metasenv subst = function | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) -> - (*D*) inside 'M'; try let rc = - pp ((if are_normal then "*" else " ") ^ " " ^ +(* (*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)); + NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2))); +*) let relevance = [] (* TO BE UNDERSTOOD match t1 with | C.Const r -> NCicEnvironment.get_relevance r @@ -439,12 +448,8 @@ and unify test_eq_only metasenv subst context t1 t2 = in try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst) with UnificationFailure _ | Uncertain _ when not are_normal -> -(* - let delta = delta - 1 in - let red = NCicReduction.reduce_machine ~delta ~subst context in -*) unif_machines metasenv subst (small_delta_step m1 m2) - (*D*) in outside(); rc with exn -> outside (); raise exn +(* (*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 -> @@ -454,7 +459,7 @@ and unify test_eq_only metasenv subst context t1 t2 = with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn -(*D*) in outside(); rc with exn -> outside (); raise exn +(* (*D*) in outside(); rc with exn -> outside (); raise exn *) ;; let unify = -- 2.39.2