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);;
+let pp s =
+ prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ s);;
+
+(* 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' =
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) ^ " in " ^ NCicPp.ppterm ~metasenv ~subst ~context t);
+ 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);
metasenv, subst, hd
(*D*) in outside (); rc with exn -> outside (); raise exn
^ 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 =
- 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
(* 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 t);
let metasenv =
List.filter (fun (m,_) -> not (n = m)) metasenv
in
| _ -> 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,
+ false (* not in normal form *)
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 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
+ let small_delta_step (_,_,t1,_ as m1) (_,_,t2,_ as m2) =
+ let h1 = height_of t1 in
+ let h2 = height_of t2 in
+ let delta =
+ if flexible [t1] then max 0 (h2 - 1) else
+ 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);
+ 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
+ (* if we have as heads a Fix of height n>m>0 and another term of height
+ * m, we set delta = m. The Fix may or may not reduce, depending on its
+ * 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);
+ 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
+ else m1', m2', delta = 0
in
let rec unif_machines metasenv subst =
function
- | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),delta) ->
+ | ((k1,e1,t1,s1 as m1),(k2,e2,t2,s2 as m2),are_normal) ->
(*D*) inside 'M'; try let rc =
- pp ((if delta > 100 then "∞" else string_of_int delta) ^ " " ^
+ pp ((if are_normal then "*" else " ") ^ " " ^
NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m1) ^
" === " ^
NCicPp.ppterm ~metasenv ~subst ~context (NCicReduction.unwind m2));
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
(NCicReduction.unwind (k2,e2,t2,List.rev l2))
in
try check_stack (List.rev s1) (List.rev s2) relevance (metasenv,subst)
- with UnificationFailure _ | Uncertain _ when delta > 0 ->
+ 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 true m1 m2)
+ 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
projects / helm.git / blobdiff