" with " ^ NCicPp.ppterm ~metasenv ~subst ~context t2))
;;
-let unify metasenv subst context t1 t2 =
+let mk_appl hd tl =
+ match hd with
+ | NCic.Appl l -> NCic.Appl (l@tl)
+ | _ -> NCic.Appl (hd :: tl)
+;;
+
+let flexible l =
+ List.exists
+ (function
+ | NCic.Meta _
+ | NCic.Appl (NCic.Meta _::_) -> true
+ | _ -> false) l
+;;
+
+exception WrongShape;;
+
+let eta_reduce after_beta_expansion after_beta_expansion_body
+ before_beta_expansion
+ =
+ try
+ match before_beta_expansion,after_beta_expansion_body with
+ Cic.Appl l, Cic.Appl l' ->
+ let rec all_but_last check_last =
+ function
+ [] -> assert false
+ | [Cic.Rel 1] -> []
+ | [_] -> if check_last then raise WrongShape else []
+ | he::tl -> he::(all_but_last check_last tl)
+ in
+ let all_but_last check_last l =
+ match all_but_last check_last l with
+ [] -> assert false
+ | [he] -> he
+ | l -> Cic.Appl l
+ in
+ let t = CicSubstitution.subst (Cic.Rel (-1)) (all_but_last true l') in
+ let all_but_last = all_but_last false l in
+ (* here we should test alpha-equivalence; however we know by
+ construction that here alpha_equivalence is equivalent to = *)
+ if t = all_but_last then
+ all_but_last
+ else
+ after_beta_expansion
+ | _,_ -> after_beta_expansion
+ with
+ WrongShape -> after_beta_expansion
+
+let rec beta_expand num test_equality_only metasenv subst context t arg ugraph =
+ let module S = CicSubstitution in
+ let module C = Cic in
+let foo () =
+ let rec aux metasenv subst n context t' ugraph =
+ try
+
+ let subst,metasenv,ugraph1 =
+ fo_unif_subst test_equality_only subst context metasenv
+ (CicSubstitution.lift n arg) t' ugraph
+
+ in
+ subst,metasenv,C.Rel (1 + n),ugraph1
+ with
+ Uncertain _
+ | UnificationFailure _ ->
+ match t' with
+ | C.Rel m -> subst,metasenv,
+ (if m <= n then C.Rel m else C.Rel (m+1)),ugraph
+ | C.Var (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,C.Var (uri,exp_named_subst'),ugraph1
+ | C.Meta (i,l) ->
+ (* andrea: in general, beta_expand can create badly typed
+ terms. This happens quite seldom in practice, UNLESS we
+ iterate on the local context. For this reason, we renounce
+ to iterate and just lift *)
+ let l =
+ List.map
+ (function
+ Some t -> Some (CicSubstitution.lift 1 t)
+ | None -> None) l in
+ subst, metasenv, C.Meta (i,l), ugraph
+ | C.Sort _
+ | C.Implicit _ as t -> subst,metasenv,t,ugraph
+ | C.Cast (te,ty) ->
+ let subst,metasenv,te',ugraph1 =
+ aux metasenv subst n context te ugraph in
+ let subst,metasenv,ty',ugraph2 =
+ aux metasenv subst n context ty ugraph1 in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Cast (te', ty')),ugraph2
+ | C.Prod (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Prod (nn, s', t')),ugraph2
+ | C.Lambda (nn,s,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Decl s))::context) t ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.Lambda (nn, s', t')),ugraph2
+ | C.LetIn (nn,s,ty,t) ->
+ let subst,metasenv,s',ugraph1 =
+ aux metasenv subst n context s ugraph in
+ let subst,metasenv,ty',ugraph1 =
+ aux metasenv subst n context ty ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst (n+1) ((Some (nn, C.Def (s,ty)))::context) t
+ ugraph1
+ in
+ (* TASSI: sure this is in serial? *)
+ subst,metasenv,(C.LetIn (nn, s', ty', t')),ugraph2
+ | C.Appl l ->
+ let subst,metasenv,revl',ugraph1 =
+ List.fold_left
+ (fun (subst,metasenv,appl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::appl),ugraph1
+ ) (subst,metasenv,[],ugraph) l
+ in
+ subst,metasenv,(C.Appl (List.rev revl')),ugraph1
+ | C.Const (uri,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.Const (uri,exp_named_subst')),ugraph1
+ | C.MutInd (uri,i,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutInd (uri,i,exp_named_subst')),ugraph1
+ | C.MutConstruct (uri,i,j,exp_named_subst) ->
+ let subst,metasenv,exp_named_subst',ugraph1 =
+ aux_exp_named_subst metasenv subst n context exp_named_subst ugraph
+ in
+ subst,metasenv,(C.MutConstruct (uri,i,j,exp_named_subst')),ugraph1
+ | C.MutCase (sp,i,outt,t,pl) ->
+ let subst,metasenv,outt',ugraph1 =
+ aux metasenv subst n context outt ugraph in
+ let subst,metasenv,t',ugraph2 =
+ aux metasenv subst n context t ugraph1 in
+ let subst,metasenv,revpl',ugraph3 =
+ List.fold_left
+ (fun (subst,metasenv,pl,ugraph) t ->
+ let subst,metasenv,t',ugraph1 =
+ aux metasenv subst n context t ugraph in
+ subst,metasenv,(t'::pl),ugraph1
+ ) (subst,metasenv,[],ugraph2) pl
+ in
+ subst,metasenv,(C.MutCase (sp,i,outt', t', List.rev revpl')),ugraph3
+ (* TASSI: not sure this is serial *)
+ | 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,(CicSubstitution.lift 1 t' ),ugraph
+ | 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,(CicSubstitution.lift 1 t'), ugraph
+
+ and aux_exp_named_subst metasenv subst n context ens ugraph =
+ List.fold_right
+ (fun (uri,t) (subst,metasenv,l,ugraph) ->
+ let subst,metasenv,t',ugraph1 = aux metasenv subst n context t ugraph in
+ subst,metasenv,((uri,t')::l),ugraph1) ens (subst,metasenv,[],ugraph)
+ in
+ let argty,ugraph1 = type_of_aux' metasenv subst context arg ugraph in
+ let fresh_name =
+ FreshNamesGenerator.mk_fresh_name ~subst
+ metasenv context (Cic.Name ("Hbeta" ^ string_of_int num)) ~typ:argty
+ in
+ let subst,metasenv,t',ugraph2 = aux metasenv subst 0 context t ugraph1 in
+ let t'' = eta_reduce (C.Lambda (fresh_name,argty,t')) t' t in
+ subst, metasenv, t'', ugraph2
+in profiler_beta_expand.HExtlib.profile foo ()
+
+
+and beta_expand_many test_equality_only metasenv subst context t args ugraph =
+ let _,subst,metasenv,hd,ugraph =
+ List.fold_right
+ (fun arg (num,subst,metasenv,t,ugraph) ->
+ let subst,metasenv,t,ugraph1 =
+ beta_expand num test_equality_only
+ metasenv subst context t arg ugraph
+ in
+ num+1,subst,metasenv,t,ugraph1
+ ) args (1,subst,metasenv,t,ugraph)
+ in
+ subst,metasenv,hd,ugraph
+
+
+
+let rec instantiate test_eq_only metasenv subst context n lc t swap =
+ let unif m s c t1 t2 =
+ if swap then unify m s c t2 t1 else unify m s c t1 t2
+ in
+ let ty_t =
+ try NCicTypeChecker.typeof ~subst ~metasenv context t
+ with NCicTypeChecker.TypeCheckerFailure _ -> assert false
+ in
+ let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
+ let ty = NCicSubstitution.subst_meta lc ty in
+ let metasenv, subst = unify metasenv susbt context ty ty_t in
+ let (metasenv, subst), t =
+ NCicMetaSubst.delift metasenv subst context n lc t
+ in
+ (* Unifying the types may have already instantiated n. *)
+ try
+ let _, _,oldt,_ = CicUtil.lookup_subst n subst in
+ let oldt = NCicSubstitution.subst_meta lc oldt in
+ (* conjecture: always fail --> occur check *)
+ unify test_eq_only metasenv subst context oldt t
+ with CicUtil.Subst_not_found _ ->
+ (* by cumulativity when unify(?,Type_i)
+ * we could ? := Type_j with j <= i... *)
+ let subst = (n, (name, ctx, t, ty)) :: subst in
+ let metasenv =
+ List.filter (fun (m,_) -> not (n = m)) metasenv
+ in
+ subst, metasenv
+
+and unify metasenv subst context t1 t2 =
let rec aux test_eq_only metasenv subst context t1 t2 =
let fo_unif test_eq_only metasenv subst t1 t2 =
if t1 === t2 then
aux test_eq_only metasenv subst context term1 term2
with NCicUtils.Subst_not_found _-> raise (UnificationFailure msg))
- | C.Meta (n1,l1), _
- | _, C.Meta (n2,l2) ->
+ | C.Meta (n,lc), t ->
+ try
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ aux test_eq_only metasenv subst context term t
+ with NCicUtils.Subst_not_found _->
+ instantiate test_eq_only metasenv subst context n lc t false
+
+ | t, C.Meta (n,lc) ->
+ try
+ let _,_,term,_ = NCicUtils.lookup_subst n subst in
+ let term = NCicSubstitution.subst_meta lc term in
+ aux test_eq_only metasenv subst context t term
+ with NCicUtils.Subst_not_found _->
+ instantiate test_eq_only metasenv subst context n lc t true
+ | NCic.Appl (NCic.Meta (i,l)::args), _ when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ aux test_eq_only metasenv subst context (mk_appl term args) t2
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when List.mem_assoc i subst ->
+ let _,_,term,_ = NCicUtils.lookup_subst i subst in
+ let term = NCicSubstitution.subst_meta l term in
+ aux test_eq_only metasenv subst context t1 (mk_appl term args)
+ | NCic.Appl (NCic.Meta (i,_)::_ as l1),
+ NCic.Appl (NCic.Meta (j,_)::_ as l2) when i=j ->
+ try
+ List.fold_left2
+ (fun (metasenv, subst) t1 t2 ->
+ aux test_eq_only metasenv subst context t1 t2)
+ (metasenv,subst) l1 l2
+ with Invalid_argument _ ->
+ raise (fail_exc metasenv subst context t1 t2)
- (try
- let _,_,term,_ = NCicUtils.lookup_subst n1 subst in
- let term = NCicSubstitution.subst_meta l1 term in
- aux test_eq_only metasenv subst context term t2
- with NCicUtils.Subst_not_found _ ->
-
- )
- (try
- let _,_,term,_ = NCicUtils.lookup_subst n2 subst in
- let term = NCicSubstitution.subst_meta l2 term in
- aux test_eq_only metasenv subst context t1 term
- with NCicUtils.Subst_not_found _ -> false)
-
+ | NCic.Appl (NCic.Meta (i,l)::args), _ when not (flexible args) ->
+ (* we verify that none of the args is a Meta,
+ since beta expanding w.r.t a metavariable makes no sense *)
+ let subst, metasenv, beta_expanded =
+ beta_expand_many
+ test_equality_only metasenv subst context t2 args ugraph
+ in
+ aux test_eq_only metasenv subst context
+ (C.Meta (i,l)) beta_expanded
+ | _, NCic.Appl (NCic.Meta (i,l)::args) when not(flexible args) ->
+ let subst,metasenv,beta_expanded =
+ beta_expand_many
+ test_equality_only
+ metasenv subst context t1 args ugraph
+ in
+ fo_unif_subst test_equality_only subst context metasenv
+ (C.Meta (i,l)) beta_expanded ugraph1
+ | _,_ ->
+.......
| (C.Appl ((C.Const r1) as _hd1::tl1), C.Appl (C.Const r2::tl2))
when (Ref.eq r1 r2 &&
List.length (E.get_relevance r1) >= List.length tl1) ->
projects / helm.git / commitdiff