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
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) ->
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
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
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 (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;;
projects / helm.git / blobdiff