Permalink
Browse files

Working on diag

I do not think I can make this work with a substitution. Instead,
perform fine grained replacement in the conclusion while folding
through the split tree
  • Loading branch information...
1 parent fd2240e commit 572767908e534cd2e1fafa1a5d39786f006b6154 @braibant committed Mar 22, 2013
Showing with 64 additions and 57 deletions.
  1. +64 −57 invert.ml4
View
@@ -1,4 +1,5 @@
let pp_constr fmt x = Pp.pp_with fmt (Printer.pr_constr x)
+let pp_constr_env env fmt x = Pp.pp_with fmt (Termops.print_constr_env env x)
let pp_gl fmt x = Pp.pp_with fmt (Printer.pr_goal x)
let pp_id fmt x = Pp.pp_with fmt (Names.Id.print x)
let pp_name fmt = function
@@ -7,19 +8,26 @@ let pp_name fmt = function
let pp_list pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a; " pp x) l
let pp_list_nl pp fmt l = List.iter (fun x -> Format.fprintf fmt "%a;\n" pp x) l
let pp_constrs fmt l = (pp_list pp_constr) fmt l
+let pp_rel_context fmt ctx =
+ let rec aux = function
+ | [] -> ()
+ | (name, _, ty)::q -> Format.fprintf fmt "%a:\t%a\n" pp_name name pp_constr ty;
+ aux q
+ in
+ aux (List.rev ctx)
let debug = true
let sanity env sigma t =
if debug
then
begin
- Format.eprintf "===\nTyping:%a\n%!" pp_constr t;
+ Format.eprintf "===\nTyping:%a\n%!" (pp_constr) t;
try
let ty = Typing.type_of env sigma t in
- Format.eprintf "Type:%a\n%!" pp_constr ty
+ Format.eprintf "Type:%a\n%!" (pp_constr) ty
with e ->
- Format.eprintf "Unable to type the term!\n"; raise e
+ Format.eprintf "Unable to type the term!\n"
end
@@ -160,8 +168,10 @@ let mk_match env sigma ind constructor params term return_clause kt kf =
let t = Term.mkCase (case_info,return_clause,term,branches) in
t
-(* Both branches of this function should behave the same, but we keep
- it to debug the construction of the [mkCase] function. *)
+(* This function is used to create the abstraction in mkCase
+ branches. Both branches of this function should behave the same,
+ but we keep it to debug the construction of the [mkCase]
+ function. *)
let debug_mk_lambdas term args_ty =
if false
then
@@ -184,42 +194,25 @@ let depends_on k ctx =
|| fold (pred k) ctx
in
fold (k + List.length ctx) ctx
-
-(** The return clause that we builds depends on the shape of the
- rel_context [ctx]. The rel_context contains the last binding
- first, so we must process it in reverse order. Then, we fold
- through the rel_context, and only
-*)
-let filter_return_clause ctx sort =
- let rec depends_on k rctx =
+(** Given a rel_context, filter_deps keeps only the elements that are
+ used dependently *)
+let filter_deps ctx =
+ let rec aux ctx rctx =
match rctx with
- | [] -> false
- | (id,Some b,t) :: rctx ->
- not (Term.noccurn k b) || not (Term.noccurn k t) || depends_on (succ k) rctx
- | (id,None,t) :: rctx ->
- not (Term.noccurn k t) || depends_on (succ k) rctx
- in
- let lift_rctx rctx =
- List.rev (Termops.lift_rel_context (-1) (List.rev rctx))
- in
- let rec aux rctx ctx =
- match rctx with
- | [] -> Term.mkArity (ctx, sort)
+ | [] -> List.rev rctx
| t :: q ->
if depends_on 1 q
then aux q (t :: ctx)
- else aux (lift_rctx q) ctx
+ else aux (Termops.lift_rel_context (-1) q) ctx
in
- aux (List.rev ctx) []
-
-(** The catch all-cases must also filter the context, to comply with
- the return clause generated by the [filter_return_clause]
- function. *)
-let mk_devil
-
-
+ aux ctx []
+(** The return clause that we builds depends on the shape of the
+ rel_context [ctx].
+*)
+let filter_return_clause ctx sort =
+ Term.mkArity (filter_deps ctx, sort)
(* construct the term fun x => match x with | t => a | _ => False -> True end *)
@@ -248,18 +241,29 @@ let diag env sigma (leaf_ids: Names.Id.t list)
* foo, it is useless to destruct (S m) if we have I (S m) (Fin.F1)
*)
| [], [] -> (* Not dependent inductive *)
+ Format.eprintf "[],[]\n";
let () = assert (CList.is_empty identifier_list) in
- let _ = List.iter (fun (id,t) -> Format.eprintf "%a => %a" pp_id id pp_constr t) substitution in
- Term.replace_vars substitution (Term.lift shift concl)
- | ll, (_,Some _,_)::stt ->
+ let _ =
+ Format.eprintf "substitution: ";
+ List.iter (fun (id,t) -> Format.eprintf "%a => %a, " pp_id id pp_constr t) substitution;
+ Format.eprintf "\n"
+ in
+ let term = Term.replace_vars substitution (Term.lift shift concl) in
+ Format.eprintf "return:%a\n" pp_constr term;
+ term
+ | ll, (_,Some _,_)::stt ->
Format.eprintf "Warning: constructor with let_ins in inversion/build_diag.\n";
build_diag env substitution identifier_list shift stl stt
- | head::ll, (name_argx,None,ty_argx)::stt ->
+ | head::ll, ((name_argx,None,ty_argx) as rel) ::stt ->
let lift_subst = List.map (fun (id, tm) -> (id, Term.lift 1 tm)) substitution in
begin match head with
| Some (ind, constructor, params, split_trees) ->
- let _ = Format.eprintf "C = %a, " pp_constr (Term.mkConstruct (ind,constructor)) in
+ Format.eprintf "C = %a, %a : %a\n" pp_constr (Term.mkConstruct (ind,constructor))
+ pp_name name_argx
+ pp_constr ty_argx;
begin
+ (* The function that is used to build the term in the
+ matching branch of the case *)
let kt args_ty =
let env' = Environ.push_rel_context args_ty env in
let stt = List.map (Term.map_rel_declaration (Term.lift 1)) stt in
@@ -269,10 +273,11 @@ let diag env sigma (leaf_ids: Names.Id.t list)
(split_trees@ll)
(args_ty@stt)
in
+ Format.eprintf "\n[kt] rel_context:%a\nterm:%a\n" pp_rel_context args_ty pp_constr term;
debug_mk_lambdas term args_ty
in
- (* otherwise, in the underscore case, we return [False -> True] *)
- let kf args_ty = Term.it_mkLambda_or_LetIn devil (args_ty@stt) in
+ (* The function that is used to build the term in the non-matching branches of the case *)
+ let kf args_ty = Term.it_mkLambda_or_LetIn devil (args_ty@ (filter_deps stt)) in
let return_clause =
let ind_family = Inductiveops.make_ind_family (ind, params) in
let ctx_ind = Inductiveops.make_arity_signature env true ind_family in
@@ -281,32 +286,36 @@ let diag env sigma (leaf_ids: Names.Id.t list)
(filter_return_clause stt concl_sort)
ctx_ind
in
- let term = mk_match env sigma ind constructor params (Term.mkRel 1) return_clause kt kf in
-
+ let term = mk_match env sigma ind constructor params (Term.mkRel 1) return_clause kt kf in
if depends_on 1 stt
then
begin
Format.eprintf "dependent branch for %a\n" pp_name name_argx;
- let t = Term.mkLambda (name_argx, ty_argx, term)
+ let t = Term.mkLambda (name_argx, ty_argx, Term.lift 1 term)
in
(sanity env sigma t; t)
end
else
begin
- Format.eprintf "non-dependent branch for %a\n" pp_name name_argx;
- term
+ Format.eprintf "non-dependent branch\n";
+ sanity (Environ.push_rel rel env) sigma term; term
end
end
| None ->
match identifier_list with
- | [] -> Errors.anomaly (Pp.str "build_diag: Less variable than split_tree leaf")
+ | [] -> Errors.anomaly (Pp.str "build_diag: Less variable than split_tree leaves")
|id_h :: id_q ->
- Format.eprintf "strange_branch %a : %a\n" pp_name name_argx pp_constr ty_argx;
- Term.mkLambda
- (name_argx, ty_argx,
- build_diag env ((id_h, Term.mkRel 1):: lift_subst) id_q (succ shift) ll stt
- )
+ if depends_on 1 stt
+ then
+ begin
+ Term.mkLambda
+ (name_argx, ty_argx,
+ build_diag env ((id_h, Term.mkRel 1):: lift_subst) id_q (succ shift) ll stt
+ )
+ end
+ else
+ build_diag env ((id_h, Term.mkRel 1) :: lift_subst) id_q (succ shift) ll stt
end
in
build_diag env [] leaf_ids 0 split_trees split_tree_types
@@ -337,13 +346,11 @@ let invert h gl =
let ctx = List.rev_append rev_ctx [Names.Name h, None, h_ty] in
diag env sigma leaves_ids split_trees ctx concl (Termops.new_sort_in_family sort_family) in
let return_clause =
- let args_ty =
- (Inductiveops.make_arity_signature env true ind_family)
- in
+ let args_ty = Inductiveops.make_arity_signature env true ind_family in
(Term.it_mkLambda_or_LetIn
(Term.mkApp ((Term.mkApp (return_pred, generalized_hyps)),
- Termops.extended_rel_vect 0 args_ty))
- args_ty)
+ Termops.extended_rel_vect 0 (filter_deps args_ty)))
+ (args_ty))
in
let _ = Format.printf "diag: %a\n" pp_constr return_clause in

0 comments on commit 5727679

Please sign in to comment.