(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 module S = CicSubstitution in
+ let module C = Cic in
+ let rec aux metasenv subst n context t' =
+ try
+ let subst,metasenv =
+ fo_unif_subst test_equality_only subst context metasenv arg t'
+ in
+ subst,metasenv,C.Rel (1 + n)
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+ match t' with
+ | C.Rel m -> subst,metasenv, if m <= n then C.Rel m else C.Rel (m+1)
+ | C.Var (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.Var (uri,exp_named_subst')
+ | C.Meta (i,l) as t->
+ (try
+ let t' = List.assoc i subst in
+ aux metasenv subst n context t'
+ with
+ Not_found -> subst,metasenv,t)
+ | C.Sort _
+ | C.Implicit _ as t -> subst,metasenv,t
+ | C.Cast (te,ty) ->
+ let subst,metasenv,te' = aux metasenv subst n context te in
+ let subst,metasenv,ty' = aux metasenv subst n context ty in
+ subst,metasenv,C.Cast (te', ty')
+ | C.Prod (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ in
+ subst,metasenv,C.Prod (nn, s', t')
+ | C.Lambda (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ in
+ subst,metasenv,C.Lambda (nn, s', t')
+ | C.LetIn (nn,s,t) ->
+ let subst,metasenv,s' = aux metasenv subst n context s in
+ let subst,metasenv,t' =
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,None)))::context) t
+ in
+ subst,metasenv,C.LetIn (nn, s', t')
+ | C.Appl l ->
+ let subst,metasenv,revl' =
+ List.fold_left
+ (fun (subst,metasenv,appl) t ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,t'::appl
+ ) (subst,metasenv,[]) l
+ in
+ subst,metasenv,C.Appl (List.rev revl')
+ | C.Const (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.MutInd (uri,i,exp_named_subst')
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst' =
+ aux_exp_named_subst metasenv subst n context exp_named_subst
+ in
+ subst,metasenv,C.MutConstruct (uri,i,j,exp_named_subst')
+ | C.MutCase (sp,i,outt,t,pl) ->
+ let subst,metasenv,outt' = aux metasenv subst n context outt in
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ let subst,metasenv,revpl' =
+ List.fold_left
+ (fun (subst,metasenv,pl) t ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,t'::pl
+ ) (subst,metasenv,[]) pl
+ in
+ subst,metasenv,C.MutCase (sp,i,outt', t', List.rev revpl')
+ | C.Fix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,i,ty,bo) -> (name, i, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.Fix (i, substitutedfl)
+*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+ | C.CoFix (i,fl) ->
+(*CSC: not implemented
+ let tylen = List.length fl in
+ let substitutedfl =
+ List.map
+ (fun (name,ty,bo) -> (name, aux n ty, aux (n+tylen) bo))
+ fl
+ in
+ C.CoFix (i, substitutedfl)
+*) subst,metasenv,CicMetaSubst.lift subst 1 t'
+
+ and aux_exp_named_subst metasenv subst n context ens =
+ List.fold_right
+ (fun (uri,t) (subst,metasenv,l) ->
+ let subst,metasenv,t' = aux metasenv subst n context t in
+ subst,metasenv,(uri,t')::l) ens (subst,metasenv,[])
+ in
+ let argty =
+ T.type_of_aux' metasenv context arg
+ in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name
+ metasenv context (Cic.Name "Heta") ~typ:argty
+ in
+ 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 =
+ List.fold_left
+ (fun (subst,metasenv,t) arg ->
+ eta_expand test_equality_only metasenv subst context t arg
+ ) (subst,metasenv,t)
+
(* NUOVA UNIFICAZIONE *)
(* A substitution is a (int * Cic.term) list that associates a
metavariable i with its body.
a new substitution which is _NOT_ unwinded. It must be unwinded before
applying it. *)
-let rec fo_unif_subst test_equality_only subst context metasenv t1 t2 =
+and fo_unif_subst test_equality_only subst context metasenv t1 t2 =
let module C = Cic in
let module R = CicMetaSubst in
let module S = CicSubstitution in
fo_unif_subst
test_equality_only subst context metasenv t2 (S.subst s1 t1)
| (C.Appl l1, C.Appl l2) ->
- let lr1 = List.rev l1 in
- let lr2 = List.rev l2 in
- let rec fo_unif_l test_equality_only subst metasenv =
- function
- [],_
- | _,[] -> assert false
- | ([h1],[h2]) ->
- fo_unif_subst test_equality_only subst context metasenv h1 h2
- | ([h],l)
- | (l,[h]) ->
- fo_unif_subst
- test_equality_only subst context metasenv h (C.Appl (List.rev l))
- | ((h1::l1),(h2::l2)) ->
- let subst', metasenv' =
- fo_unif_subst test_equality_only subst context metasenv h1 h2
- in
- fo_unif_l test_equality_only subst' metasenv' (l1,l2)
+ let subst,metasenv,t1',t2' =
+ match l1,l2 with
+ (* 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, _ ->
+ let subst,metasenv,t2' =
+ eta_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
+ in
+ subst,metasenv,t1',t2
+ | _,_ -> subst,metasenv,t1,t2
in
- fo_unif_l test_equality_only subst metasenv (lr1, lr2)
+ begin
+ match t1',t2' with
+ C.Appl l1, C.Appl l2 ->
+ let lr1 = List.rev l1 in
+ let lr2 = List.rev l2 in
+ let rec fo_unif_l test_equality_only subst metasenv =
+ function
+ [],_
+ | _,[] -> assert false
+ | ([h1],[h2]) ->
+ fo_unif_subst test_equality_only subst context metasenv h1 h2
+ | ([h],l)
+ | (l,[h]) ->
+ fo_unif_subst
+ test_equality_only subst context metasenv h (C.Appl (List.rev l))
+ | ((h1::l1),(h2::l2)) ->
+ let subst', metasenv' =
+ fo_unif_subst test_equality_only subst context metasenv h1 h2
+ in
+ fo_unif_l test_equality_only subst' metasenv' (l1,l2)
+ in
+ fo_unif_l test_equality_only subst metasenv (lr1, lr2)
+ | _ -> assert false
+ end
| (C.MutCase (_,_,outt1,t1',pl1), C.MutCase (_,_,outt2,t2',pl2))->
let subst', metasenv' =
fo_unif_subst test_equality_only subst context metasenv outt1 outt2 in
projects / helm.git / blobdiff