(CicMetaSubst.ppcontext subst context)
(CicMetaSubst.ppmetasenv metasenv subst) msg)))
-let rec eta_expand test_equality_only metasenv subst context t arg =
- let module T = CicTypeChecker in
+let rec beta_expand test_equality_only metasenv subst context t arg =
let module S = CicSubstitution in
let module C = Cic in
let rec aux metasenv subst n context t' =
+(*prerr_endline ("1 ciclo di beta_expand arg=" ^ CicMetaSubst.ppterm subst arg ^ " ; term=" ^ CicMetaSubst.ppterm subst t') ;*)
try
let subst,metasenv =
fo_unif_subst test_equality_only subst context metasenv arg t'
subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
in
let argty =
- T.type_of_aux' metasenv context arg
+ type_of_aux' metasenv subst context arg
in
let fresh_name =
FreshNamesGenerator.mk_fresh_name
let subst,metasenv,t' = aux metasenv subst 0 context t in
subst,metasenv, C.Appl [C.Lambda (fresh_name,argty,t') ; arg]
-and eta_expand_many test_equality_only metasenv subst context t =
+and beta_expand_many test_equality_only metasenv subst context t =
List.fold_left
(fun (subst,metasenv,t) arg ->
- eta_expand test_equality_only metasenv subst context t arg
+ beta_expand test_equality_only metasenv subst context t arg
) (subst,metasenv,t)
(* NUOVA UNIFICAZIONE *)
(try
let subst,metasenv =
fo_unif_subst
- test_equality_only subst context metasenv t1' t2'
+ test_equality_only subst context metasenv t1' t2'
in
true,subst,metasenv
with
let fo_unif_subst_ordered
test_equality_only subst context metasenv m1 m2 =
fo_unif_subst test_equality_only subst context metasenv
- (lower m1 m2) (upper m1 m2)
+ (lower m1 m2) (upper m1 m2)
in
- let subst'',metasenv' =
+ begin
try
let oldt = (List.assoc n subst) in
let lifted_oldt = S.lift_meta l oldt in
fo_unif_subst_ordered
- test_equality_only subst context metasenv t lifted_oldt
+ test_equality_only subst context metasenv t lifted_oldt
with Not_found ->
- 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'' =
- 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
- ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
- s
- | _ -> t'
- in
- (n, t'')::subst', metasenv'
- in
- let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in
- (try
- let tyt =
- type_of_aux' metasenv' subst'' context t
- in
- fo_unif_subst
- test_equality_only
- subst'' context metasenv' tyt (S.lift_meta l meta_type)
- with AssertFailure _ ->
- (* 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)
- *)
+ (* First of all we unify the type of the meta with the type of the term *)
+ let subst,metasenv =
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
+ (try
+ let tyt =
+ type_of_aux' metasenv subst context t
+ in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv tyt (S.lift_meta l meta_type)
+ with AssertFailure _ ->
+ (* 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)
+ *)
(*
prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
*)
- (subst'', metasenv'))
+ (subst, metasenv))
+ 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'' =
+ 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
+ ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
+ s
+ | _ -> t'
+ in
+ (* Unifying the types may have already instantiated n. Let's check *)
+ try
+ let oldt = (List.assoc n subst) in
+ let lifted_oldt = S.lift_meta l oldt in
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt
+ with
+ Not_found ->
+ (n,t'')::subst, metasenv
+ 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
| (C.Appl l1, C.Appl l2) ->
let subst,metasenv,t1',t2' =
match l1,l2 with
+ C.Meta (i,_)::_, C.Meta (j,_)::_ when i = j ->
+ subst,metasenv,t1,t2
(* In the first two cases when we reach the next begin ... end
section useless work is done since, by construction, the list
of arguments will be equal.
*)
- C.Meta (i,l)::args, _ ->
+ | C.Meta (i,l)::args, _ ->
let subst,metasenv,t2' =
- eta_expand_many test_equality_only metasenv subst context t2 args
+ beta_expand_many test_equality_only metasenv subst context t2 args
in
subst,metasenv,t1,t2'
| _, C.Meta (i,l)::args ->
let subst,metasenv,t1' =
- eta_expand_many test_equality_only metasenv subst context t1 args
+ beta_expand_many test_equality_only metasenv subst context t1 args
in
subst,metasenv,t1',t2
- | _,_ -> subst,metasenv,t1,t2
+ | _,_ ->
+ subst,metasenv,t1,t2
in
begin
match t1',t2' with
projects / helm.git / blobdiff