From 0126a3d56c31231c38367ad7190fe80e471ca8cc Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 29 Sep 2009 17:28:24 +0000 Subject: [PATCH] 1) improved (???) debugging, with 1.1 more messages (good) 1.2 messages for exceptions (very good) 1.3 vim folding/unfolding (good or very bad?) 2) bug partially fixed (to be improved/totally fixed): when we unify a ?n:? vs a term t, we need to check that t is a sort! (or a flexible term??? what to do in that case?) otherwise we can get ?n := O and ?1:?2:?n=0 which is a not well typed metasenv. Hence boom later. --- .../components/ng_refiner/nCicUnification.ml | 73 ++++++++++++++----- 1 file changed, 56 insertions(+), 17 deletions(-) diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index cf44ff470..a3c980648 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -78,21 +78,27 @@ let eta_reduce subst t = module C = NCic;; module Ref = NReference;; +let debug = false;; let indent = ref "";; -let inside c = indent := !indent ^ String.make 1 c;; -let outside () = +let pp = + if debug then + fun s -> prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) + else + fun _ -> () +;; +let inside c = + indent := !indent ^ String.make 1 c; + if debug then prerr_endline ("{{{" ^ !indent ^ " ") +;; +let outside ok = + if debug then prerr_endline "}}}"; + if not ok then pp (lazy "exception raised!"); try indent := String.sub !indent 0 (String.length !indent -1) with Invalid_argument _ -> indent := "??"; () ;; -let pp s = - prerr_endline (Printf.sprintf "%-20s" !indent ^ " " ^ Lazy.force s) -;; - -let pp _ = ();; - let ppcontext ~metasenv ~subst c = "\nctx:\n"^ NCicPp.ppcontext ~metasenv ~subst c ;; @@ -186,7 +192,38 @@ and instantiate rdb test_eq_only metasenv subst context n lc t swap = let metasenv, subst, t = match ty with | NCic.Implicit (`Typeof _) -> - metasenv,subst, t + (let ty_t = + try + t (* + NCicTypeChecker.typeof ~subst ~metasenv context t*) + with + NCicTypeChecker.AssertFailure msg -> + let exc_to_be = + fail_exc metasenv subst context (NCic.Meta (n,lc)) t in + pp (lazy "fine typeof (fallimento)"); + let ft = fix_sorts swap exc_to_be t in + if ft == t then + (prerr_endline ( ("ILLTYPED: " ^ + NCicPp.ppterm ~metasenv ~subst ~context t + ^ "\nBECAUSE:" ^ Lazy.force msg ^ + ppcontext ~metasenv ~subst context ^ + ppmetasenv ~subst metasenv + )); + assert false) + else + (try + pp (lazy ("typeof: " ^ + NCicPp.ppterm ~metasenv ~subst ~context ft)); + NCicTypeChecker.typeof ~subst ~metasenv context ft + with NCicTypeChecker.AssertFailure _ -> + assert false) + | NCicTypeChecker.TypeCheckerFailure _ -> assert false + in + match NCicReduction.whd ~subst context ty_t with + NCic.Sort _ -> metasenv,subst, t + | NCic.Meta _ -> metasenv,subst,t (* CSC: TO BE IMPLEMENTED *) + | _ -> raise (Uncertain (lazy "Trying to instantiate a metavariable that represents a sort with a term"))) + (*CSC: TO BE IMPLEMENTED: UnificationFailure of string Lazy.t;; *) (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *) | _ -> pp (lazy ( @@ -282,7 +319,7 @@ and instantiate rdb 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 + (*D*) in outside true; rc with exn -> outside false; raise exn and unify rdb test_eq_only metasenv subst context t1 t2 = (*D*) inside 'U'; try let rc = @@ -541,9 +578,10 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = NCicUntrusted.metas_of_term subst context t2 = [] -> raise (fail_exc metasenv subst context t1 t2) | _ -> raise (uncert_exc metasenv subst context t1 t2) - (*D*) in outside(); rc with exn -> outside (); raise exn + (*D*) in outside true; rc with exn -> outside false; raise exn in let try_hints metasenv subst t1 t2 (* exc*) = + (*D*) inside 'H'; try let rc = (* prerr_endline ("\nProblema:\n" ^ NCicPp.ppterm ~metasenv ~subst ~context t1 ^ " =?= " ^ @@ -555,8 +593,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = let rec cand_iter = function | [] -> None (* raise exc *) | (metasenv,(c1,c2),premises)::tl -> -(* - prerr_endline ("\nProvo il candidato:\n" ^ + pp (lazy ("\nProvo il candidato:\n" ^ String.concat "\n" (List.map (fun (a,b) -> @@ -564,9 +601,9 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = NCicPp.ppterm ~metasenv ~subst ~context b) premises) ^ "\n-------------------------------------------\n"^ NCicPp.ppterm ~metasenv ~subst ~context c1 ^ " = " ^ - NCicPp.ppterm ~metasenv ~subst ~context c2); -*) + NCicPp.ppterm ~metasenv ~subst ~context c2)); try + (*D*) inside 'K'; try let rc = let metasenv,subst = fo_unif test_eq_only metasenv subst t1 c1 in let metasenv,subst = @@ -578,11 +615,13 @@ and unify rdb test_eq_only metasenv subst context t1 t2 = (metasenv, subst) premises in Some (metasenv, subst) + (*D*) in outside true; rc with exn -> outside false; raise exn with UnificationFailure _ | Uncertain _ -> cand_iter tl in cand_iter candidates + (*D*) in outside true; rc with exn -> outside false; raise exn in let height_of = function | NCic.Const (Ref.Ref (_,Ref.Def h)) @@ -651,7 +690,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); ) (metasenv,subst) todo with UnificationFailure _ | Uncertain _ when not (norm1 && norm2) -> unif_machines metasenv subst (small_delta_step ~subst m1 m2) - (*D*) in outside(); rc with exn -> outside (); raise exn + (*D*) in outside true; rc with exn -> outside false; raise exn in try fo_unif test_eq_only metasenv subst t1 t2 with @@ -672,7 +711,7 @@ pp (lazy (string_of_bool norm1 ^ " ?? " ^ string_of_bool norm2)); with | UnificationFailure _ -> raise (UnificationFailure msg) | Uncertain _ -> raise exn - (*D*) in outside(); rc with exn -> outside (); raise exn + (*D*) in outside true; rc with exn -> outside false; raise exn and delift_type_wrt_terms rdb metasenv subst context t args = let (metasenv, subst), t = -- 2.39.2