-
-let beta_expand ?(metas_ok=true) ?(match_only=false)
- what type_of_what where context metasenv ugraph =
- let module S = CicSubstitution in
- let module C = Cic in
-
-(* let _ = *)
-(* let names = names_of_context context in *)
-(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
-(* (CicPp.pp what names) (CicPp.ppterm what) *)
-(* (CicPp.pp where names) (CicPp.ppterm where); *)
-(* print_newline (); *)
-(* in *)
- (*
- return value:
- ((list of all possible beta expansions, subst, metasenv, ugraph),
- lifted term)
- *)
- let rec aux lift_amount term context metasenv subst ugraph =
-(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *)
- let res, lifted_term =
- match term with
- | C.Rel m ->
- [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
-
- | C.Var (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Var (uri, e), s, m, ug)) ens'
- in
- expansions, C.Var (uri, lifted_ens)
-
- | C.Meta (i, l) ->
- let l', lifted_l =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- match arg with
- | Some arg ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug)
- arg_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug)
- res),
- (Some lifted_arg)::lifted_tl)
- | None ->
- (List.map
- (fun (r, s, m, ug) -> None::r, s, m, ug)
- res,
- None::lifted_tl)
- ) l ([], [])
- in
- let e =
- List.map
- (fun (l, s, m, ug) ->
- (C.Meta (i, l), s, m, ug)) l'
- in
- e, C.Meta (i, lifted_l)
-
- | C.Sort _
- | C.Implicit _ as t -> [], t
-
- | C.Cast (s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Cast (lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Cast (lifted_s, lifted_t)
-
- | C.Prod (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Prod (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Prod (nn, lifted_s, lifted_t)
-
- | C.Lambda (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Decl s))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.Lambda (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.Lambda (nn, lifted_s, lifted_t)
-
- | C.LetIn (nn, s, t) ->
- let l1, lifted_s =
- aux lift_amount s context metasenv subst ugraph in
- let l2, lifted_t =
- aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context)
- metasenv subst ugraph
- in
- let l1' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, t, lifted_t), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.LetIn (nn, lifted_s, t), s, m, ug) l2 in
- l1'@l2', C.LetIn (nn, lifted_s, lifted_t)
-
- | C.Appl l ->
- let l', lifted_l =
- aux_list lift_amount l context metasenv subst ugraph
- in
- (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l',
- C.Appl lifted_l)
-
- | C.Const (uri, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.Const (uri, e), s, m, ug)) ens'
- in
- (expansions, C.Const (uri, lifted_ens))
-
- | C.MutInd (uri, i ,exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutInd (uri, i, e), s, m, ug)) ens'
- in
- (expansions, C.MutInd (uri, i, lifted_ens))
-
- | C.MutConstruct (uri, i, j, exp_named_subst) ->
- let ens', lifted_ens =
- aux_ens lift_amount exp_named_subst context metasenv subst ugraph
- in
- let expansions =
- List.map
- (fun (e, s, m, ug) ->
- (C.MutConstruct (uri, i, j, e), s, m, ug)) ens'
- in
- (expansions, C.MutConstruct (uri, i, j, lifted_ens))
-
- | C.MutCase (sp, i, outt, t, pl) ->
- let pl_res, lifted_pl =
- aux_list lift_amount pl context metasenv subst ugraph
- in
- let l1, lifted_outt =
- aux lift_amount outt context metasenv subst ugraph in
- let l2, lifted_t =
- aux lift_amount t context metasenv subst ugraph in
-
- let l1' =
- List.map
- (fun (outt, s, m, ug) ->
- C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in
- let l2' =
- List.map
- (fun (t, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in
- let l3' =
- List.map
- (fun (pl, s, m, ug) ->
- C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res
- in
- (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl))
-
- | C.Fix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, idx, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, idx, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl',
- C.Fix (i, lifted_fl))
-
- | C.CoFix (i, fl) ->
- let len = List.length fl in
- let fl', lifted_fl =
- List.fold_right
- (fun (nm, ty, bo) (res, lifted_tl) ->
- let lifted_ty = S.lift lift_amount ty in
- let bo_res, lifted_bo =
- aux (lift_amount+len) bo context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) ->
- (nm, lifted_ty, a)::lifted_tl, s, m, ug)
- bo_res
- in
- (l1 @
- (List.map
- (fun (r, s, m, ug) ->
- (nm, lifted_ty, lifted_bo)::r, s, m, ug) res),
- (nm, lifted_ty, lifted_bo)::lifted_tl)
- ) fl ([], [])
- in
- (List.map
- (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl',
- C.CoFix (i, lifted_fl))
- in
- let retval =
- match term with
- | C.Meta _ when (not metas_ok) ->
- res, lifted_term
- | _ ->
-(* let term' = *)
-(* if match_only then replace_metas context term *)
-(* else term *)
-(* in *)
- try
- let subst', metasenv', ugraph' =
-(* Printf.printf "provo a unificare %s e %s\n" *)
-(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
- if match_only then
- matching metasenv context term (S.lift lift_amount what) ugraph
- else
- CicUnification.fo_unif metasenv context
- (S.lift lift_amount what) term ugraph
- in
-(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
-(* (CicPp.ppterm (S.lift lift_amount what)); *)
-(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
-(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
- (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
-(* if match_only then *)
-(* let t' = CicMetaSubst.apply_subst subst' term in *)
-(* if not (meta_convertibility term t') then ( *)
-(* res, lifted_term *)
-(* ) else ( *)
-(* let metas = metas_of_term term in *)
-(* let fix_subst = function *)
-(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
-(* (j, (c, C.Meta (i, lc), ty)) *)
-(* | s -> s *)
-(* in *)
-(* let subst' = List.map fix_subst subst' in *)
-(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
-(* lifted_term) *)
-(* ) *)
-(* else *)
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- with
- | MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ ->
- res, lifted_term
- in
-(* Printf.printf "exit aux\n"; *)
- retval
-
- and aux_list lift_amount l context metasenv subst ugraph =
- List.fold_right
- (fun arg (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 = List.map
- (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map
- (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res),
- lifted_arg::lifted_tl)
- ) l ([], [])
-
- and aux_ens lift_amount exp_named_subst context metasenv subst ugraph =
- List.fold_right
- (fun (u, arg) (res, lifted_tl) ->
- let arg_res, lifted_arg =
- aux lift_amount arg context metasenv subst ugraph in
- let l1 =
- List.map
- (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res
- in
- (l1 @ (List.map (fun (r, s, m, ug) ->
- (u, lifted_arg)::r, s, m, ug) res),
- (u, lifted_arg)::lifted_tl)
- ) exp_named_subst ([], [])
-
- in
- let expansions, _ =
-(* let where = *)
-(* if match_only then replace_metas (\* context *\) where *)
-(* else where *)
-(* in *)
- aux 0 where context metasenv [] ugraph
- in
- let mapfun =
-(* if match_only then *)
-(* (fun (term, subst, metasenv, ugraph) -> *)
-(* let term' = *)
-(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *)
-(* and subst = restore_subst subst in *)
-(* (term', subst, metasenv, ugraph)) *)
-(* else *)
- (fun (term, subst, metasenv, ugraph) ->
- let term' = C.Lambda (C.Anonymous, type_of_what, term) in
- (term', subst, metasenv, ugraph))
- in
- List.map mapfun expansions
-;;
-
-
-let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =