- subst,metasenv,hd,ugraph
-
-and warn_if_not_unique xxx to1 to2 carr car1 car2 =
- match xxx with
- | [] -> ()
- | (m2,_,c2,c2')::_ ->
- let m1,c1,c1' = carr,to1,to2 in
- let unopt =
- function Some (_,t) -> CicPp.ppterm t
- | None -> "id"
- in
- HLog.warn
- ("There are two minimal joins of "^ CoercDb.string_of_carr car1^" and "^
- CoercDb.string_of_carr car2^": " ^
- CoercDb.string_of_carr m1^" via "^unopt c1^" + "^
- unopt c1'^" and "^ CoercDb.string_of_carr m2^" via "^
- unopt c2^" + "^unopt c2')
-
-(* NUOVA UNIFICAZIONE *)
-(* A substitution is a (int * Cic.term) list that associates a
- metavariable i with its body.
- A metaenv is a (int * Cic.term) list that associate a metavariable
- i with is type.
- fo_unif_new takes a metasenv, a context, two terms t1 and t2 and gives back
- a new substitution which is _NOT_ unwinded. It must be unwinded before
- applying it. *)
-
-and fo_unif_subst test_equality_only subst context metasenv t1 t2 ugraph =
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let t1 = deref subst t1 in
- let t2 = deref subst t2 in
- let (&&&) a b = (a && b) || ((not a) && (not b)) in
-(* let bef = Sys.time () in *)
- let b,ugraph =
- if not (CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t1) &&& CicUtil.is_meta_closed (CicMetaSubst.apply_subst subst t2)) then
- false,ugraph
- else
-let foo () =
- R.are_convertible ~subst ~metasenv context t1 t2 ugraph
-in profiler_are_convertible.HExtlib.profile foo ()
- in
-(* let aft = Sys.time () in
-if (aft -. bef > 2.0) then prerr_endline ("LEEEENTO: " ^
-CicMetaSubst.ppterm_in_context subst ~metasenv t1 context ^ " <===> " ^
-CicMetaSubst.ppterm_in_context subst ~metasenv t2 context); *)
- if b then
- subst, metasenv, ugraph
- else
- match (t1, t2) with
- | (C.Meta (n,ln), C.Meta (m,lm)) when n=m ->
- let _,subst,metasenv,ugraph1 =
- (try
- List.fold_left2
- (fun (j,subst,metasenv,ugraph) t1 t2 ->
- match t1,t2 with
- None,_
- | _,None -> j+1,subst,metasenv,ugraph
- | Some t1', Some t2' ->
- (* First possibility: restriction *)
- (* Second possibility: unification *)
- (* Third possibility: convertibility *)
- let b, ugraph1 =
- R.are_convertible
- ~subst ~metasenv context t1' t2' ugraph
- in
- if b then
- j+1,subst,metasenv, ugraph1
- else
- (try
- let subst,metasenv,ugraph2 =
- fo_unif_subst
- test_equality_only
- subst context metasenv t1' t2' ugraph
- in
- j+1,subst,metasenv,ugraph2
- with
- Uncertain _
- | UnificationFailure _ ->
-debug_print (lazy ("restringo Meta n." ^ (string_of_int n) ^ "on variable n." ^ (string_of_int j)));
- let metasenv, subst =
- CicMetaSubst.restrict
- subst [(n,j)] metasenv in
- j+1,subst,metasenv,ugraph1)
- ) (1,subst,metasenv,ugraph) ln lm
- with
- Exit ->
- raise
- (UnificationFailure (lazy "1"))
- (*
- (sprintf
- "Error trying to unify %s with %s: the algorithm tried to check whether the two substitutions are convertible; if they are not, it tried to unify the two substitutions. No restriction was attempted."
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))) *)
- | Invalid_argument _ ->
- raise
- (UnificationFailure (lazy "2")))
- (*
- (sprintf
- "Error trying to unify %s with %s: the lengths of the two local contexts do not match."
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2)))) *)
- in subst,metasenv,ugraph1
- | (C.Meta (n,_), C.Meta (m,_)) when n>m ->
- fo_unif_subst test_equality_only subst context metasenv t2 t1 ugraph
- | (C.Meta (n,l), t)
- | (t, C.Meta (n,l)) ->
- let swap =
- match t1,t2 with
- C.Meta (n,_), C.Meta (m,_) when n < m -> false
- | _, C.Meta _ -> false
- | _,_ -> true
- in
- let lower = fun x y -> if swap then y else x in
- let upper = fun x y -> if swap then x else y in
- let fo_unif_subst_ordered
- test_equality_only subst context metasenv m1 m2 ugraph =
- fo_unif_subst test_equality_only subst context metasenv
- (lower m1 m2) (upper m1 m2) ugraph
- in
- begin
- let subst,metasenv,ugraph1 =
- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
- (try
- let tyt,ugraph1 =
- type_of_aux' metasenv subst context t ugraph
- in
- fo_unif_subst
- test_equality_only
- subst context metasenv tyt (S.subst_meta l meta_type) ugraph1
- with
- UnificationFailure _ as e -> raise e
- | Uncertain msg -> raise (UnificationFailure msg)
- | AssertFailure _ ->
- debug_print (lazy "siamo allo huge hack");
- (* TODO huge hack!!!!
- * we keep on unifying/refining in the hope that
- * the problem will be eventually solved.
- * In the meantime we're breaking a big invariant:
- * the terms that we are unifying are no longer well
- * typed in the current context (in the worst case
- * we could even diverge) *)
- (subst, metasenv,ugraph)) in
- let t',metasenv,subst =
- try
- CicMetaSubst.delift n subst context metasenv l t
- with
- (CicMetaSubst.MetaSubstFailure msg)->
- raise (UnificationFailure msg)
- | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
- in
- let t'',ugraph2 =
- match t' with
- C.Sort (C.Type u) when not test_equality_only ->
- let u' = CicUniv.fresh () in
- let s = C.Sort (C.Type u') in
- (try
- let ugraph2 =
- CicUniv.add_ge (upper u u') (lower u u') ugraph1
- in
- s,ugraph2
- with
- CicUniv.UniverseInconsistency msg ->
- raise (UnificationFailure msg))
- | _ -> t',ugraph1
- in
- (* Unifying the types may have already instantiated n. Let's check *)
- try
- let (_, oldt,_) = CicUtil.lookup_subst n subst in
- let lifted_oldt = S.subst_meta l oldt in
- fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt ugraph2
- with
- CicUtil.Subst_not_found _ ->
- let (_, context, ty) = CicUtil.lookup_meta n metasenv in
- let subst = (n, (context, t'',ty)) :: subst in
- let metasenv =
- List.filter (fun (m,_,_) -> not (n = m)) metasenv in
- subst, metasenv, ugraph2
- end
- | (C.Var (uri1,exp_named_subst1),C.Var (uri2,exp_named_subst2))
- | (C.Const (uri1,exp_named_subst1),C.Const (uri2,exp_named_subst2)) ->
- if UriManager.eq uri1 uri2 then
- fo_unif_subst_exp_named_subst test_equality_only subst context metasenv
- exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure (lazy
- (sprintf
- "Can't unify %s with %s due to different constants"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | C.MutInd (uri1,i1,exp_named_subst1),C.MutInd (uri2,i2,exp_named_subst2) ->
- if UriManager.eq uri1 uri2 && i1 = i2 then
- fo_unif_subst_exp_named_subst
- test_equality_only
- subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s due to different inductive principles"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | C.MutConstruct (uri1,i1,j1,exp_named_subst1),
- C.MutConstruct (uri2,i2,j2,exp_named_subst2) ->
- if UriManager.eq uri1 uri2 && i1 = i2 && j1 = j2 then
- fo_unif_subst_exp_named_subst
- test_equality_only
- subst context metasenv exp_named_subst1 exp_named_subst2 ugraph
- else
- raise (UnificationFailure
- (lazy
- (sprintf
- "Can't unify %s with %s due to different inductive constructors"
- (CicMetaSubst.ppterm ~metasenv subst t1)
- (CicMetaSubst.ppterm ~metasenv subst t2))))
- | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
- | (C.Cast (te,ty), t2) -> fo_unif_subst test_equality_only
- subst context metasenv te t2 ugraph
- | (t1, C.Cast (te,ty)) -> fo_unif_subst test_equality_only
- subst context metasenv t1 te ugraph
- | (C.Lambda (n1,s1,t1), C.Lambda (_,s2,t2)) ->
- let subst',metasenv',ugraph1 =
- fo_unif_subst test_equality_only subst context metasenv s1 s2 ugraph
+ 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 =
+ pp (lazy(string_of_int n ^ " :=?= "^
+ NCicPp.ppterm ~metasenv ~subst ~context t));
+ 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 name, ctx, ty = NCicUtils.lookup_meta n metasenv in
+ let metasenv, subst, t =
+ match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv,subst, t
+ (* fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t *)
+ | _ ->
+ pp (lazy (
+ "typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t ^ "\nctx:\n"^
+ NCicPp.ppcontext ~metasenv ~subst context ^ "\nmenv:\n"^
+ NCicPp.ppmetasenv ~subst metasenv));
+ let t, ty_t =
+ try t, NCicTypeChecker.typeof ~subst ~metasenv context t
+ with
+ | NCicTypeChecker.AssertFailure msg ->
+ (pp (lazy "fine typeof (fallimento)");
+ let ft=fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t in
+ if ft == t then
+ (prerr_endline ( ("ILLTYPED: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context t
+ ^ "\nBECAUSE:" ^ Lazy.force msg ^ "\nCONTEXT:\n" ^
+ NCicPp.ppcontext ~metasenv ~subst context ^ "\nMENV:\n" ^
+ NCicPp.ppmetasenv ~subst metasenv
+ ));
+ assert false)
+ else
+ try
+ pp (lazy ("typeof: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ft));
+ ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
+ with NCicTypeChecker.AssertFailure _ ->
+ assert false)
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ prerr_endline (Lazy.force msg);
+ pp msg; assert false