X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=a3c980648f9b87128128a815f9c01a0e85dd1ecb;hb=61948e2e9b31460eb6a0bbd627c90a6549d65414;hp=3d89161b3220a770e69582e09da11271267377f5;hpb=3a4c39fc9c938ca155f0e807525cd38eec240a0d;p=helm.git diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml index 3d89161b3..a3c980648 100644 --- a/helm/software/components/ng_refiner/nCicUnification.ml +++ b/helm/software/components/ng_refiner/nCicUnification.ml @@ -15,11 +15,6 @@ exception UnificationFailure of string Lazy.t;; exception Uncertain of string Lazy.t;; exception AssertFailure of string Lazy.t;; -let refiner_typeof = - ref (fun _ ?localise _ _ _ _ _ -> ignore localise; assert false);; -let set_refiner_typeof f = refiner_typeof := f -;; - let (===) x y = Pervasives.compare x y = 0 ;; let uncert_exc metasenv subst context t1 t2 = @@ -83,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 ;; @@ -191,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 ( @@ -287,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 = @@ -546,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 ^ " =?= " ^ @@ -560,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) -> @@ -569,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 = @@ -583,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)) @@ -656,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 @@ -677,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 =