From 1370320539f00fd49d8a6503bdb8fdbf54c4f983 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 3 Oct 2008 09:11:11 +0000 Subject: [PATCH] better debuggin output --- helm/software/components/ng_refiner/check.ml | 1 - .../components/ng_refiner/nCicUnification.ml | 45 +++++++++++++------ helm/software/components/ng_refiner/rt.ml | 1 - 3 files changed, 32 insertions(+), 15 deletions(-) diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml index 1d3408d6b..79ed2f037 100644 --- a/helm/software/components/ng_refiner/check.ml +++ b/helm/software/components/ng_refiner/check.ml @@ -73,7 +73,6 @@ let _ = prerr_endline (HelmLogger.string_of_html_msg html_msg)); CicParser.impredicative_set := false; NCicTypeChecker.set_logger logger; - NCicPp.set_ppterm NCicPp.trivial_pp_term; Helm_registry.load_from "conf.xml"; let alluris = try diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 11f90736a..51ea8809b 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -68,6 +68,12 @@ 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 ^ " " ^ s);; + 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 +117,9 @@ 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) ^ " in " ^ NCicPp.ppterm ~metasenv ~subst ~context t); let _, subst, metasenv, hd = List.fold_right (fun arg (num,subst,metasenv,t) -> @@ -121,8 +130,10 @@ and beta_expand_many test_equality_only swap metasenv subst context t args = args (1,subst,metasenv,t) in 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 @@ -136,6 +147,8 @@ 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); 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 @@ -154,12 +167,14 @@ and instantiate test_eq_only metasenv subst context n lc t swap = 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 (" " ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " === " ^ + NCicPp.ppterm ~metasenv ~subst ~context t2); if t1 === t2 then metasenv, subst else @@ -343,6 +358,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 in let height_of is_whd = function | NCic.Const (Ref.Ref (_,Ref.Def h)) @@ -362,13 +378,14 @@ and unify test_eq_only metasenv subst context t1 t2 = NCicReduction.reduce_machine ~delta ~subst context m2, if is_whd && flex1 && flex2 then 0 else delta in - let rec unif_machines metasenv subst = function + 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 + (*D*) inside 'M'; try let rc = + pp ((if delta > 100 then "∞" else string_of_int delta) ^ " " ^ + 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 @@ -395,15 +412,14 @@ 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) + try 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 + (*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 -> @@ -413,9 +429,12 @@ 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 ;; -let unify = unify false;; +let unify = + indent := ""; + unify false;; diff --git a/helm/software/components/ng_refiner/rt.ml b/helm/software/components/ng_refiner/rt.ml index 3843d5a78..997bc2e3c 100644 --- a/helm/software/components/ng_refiner/rt.ml +++ b/helm/software/components/ng_refiner/rt.ml @@ -14,7 +14,6 @@ let _ = Helm_registry.load_from "conf.xml"; CicParser.impredicative_set := false; - NCicPp.set_ppterm NCicPp.trivial_pp_term; let u = UriManager.uri_of_string Sys.argv.(1) in let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in prerr_endline "VECCHIO"; -- 2.39.2