From a7c69804c48f974f3325c03da63391189a662c50 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sun, 18 Oct 2015 15:01:42 +0200 Subject: [PATCH] Record the arity of each branch in Case constructs (not easily computable otherwise). --- src/reify.ml4 | 11 +++++++---- theories/Ast.v | 2 +- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/reify.ml4 b/src/reify.ml4 index 3aad186ab..476cee63e 100644 --- a/src/reify.ml4 +++ b/src/reify.ml4 @@ -243,10 +243,13 @@ struct let (a',acc) = quote_term acc env a in let (b',acc) = quote_term acc env b in let (branches,acc) = - List.fold_left (fun (xs,acc) x -> - let (x,acc) = quote_term acc env x in (x :: xs, acc)) - ([],acc) (Array.to_list e) in - (Term.mkApp (tCase, [| npar ; a' ; b' ; to_coq_list tTerm (List.rev branches) |]), acc) + CArray.fold_left2 (fun (xs,acc) x nargs -> + let (x,acc) = quote_term acc env x in + let t = pair tnat tTerm (int_to_nat nargs) x in + (t :: xs, acc)) + ([],acc) e ci.ci_cstr_nargs in + let tl = prod tnat tTerm in + (Term.mkApp (tCase, [| npar ; a' ; b' ; to_coq_list tl (List.rev branches) |]), acc) | Term.Fix fp -> let (t,n,acc) = quote_fixpoint acc env fp in (Term.mkApp (tFix, [| t ; int_to_nat n |]), acc) diff --git a/theories/Ast.v b/theories/Ast.v index acd603b29..0865deecd 100644 --- a/theories/Ast.v +++ b/theories/Ast.v @@ -48,7 +48,7 @@ Inductive term : Set := | tConst : string -> term | tInd : inductive -> term | tConstruct : inductive -> nat -> term -| tCase : nat (* # of parameters *) -> term (** type info **) -> term -> list term -> term +| tCase : nat (* # of parameters *) -> term (** type info **) -> term -> list (nat * term) -> term | tFix : mfixpoint term -> nat -> term (* | CoFix of ('constr, 'types) pcofixpoint