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 *)
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' =
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) ->
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
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
(* 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
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))
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
* 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
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
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 ->
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 =
projects / helm.git / commitdiff