diff options
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
-rw-r--r-- | contrib/subtac/subtac_command.ml | 77 |
1 files changed, 45 insertions, 32 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 1b92c691..b09228c0 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -55,8 +55,8 @@ let interp_gen kind isevars env ?(impls=([],[])) ?(allow_soapp=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_soapp ~ltacvars (Evd.evars_of !isevars) env c in - let c' = Subtac_interp_fixpoint.rewrite_cases env c' in - msgnl (str "Pretyping " ++ my_print_constr_expr c); + let c' = Subtac_utils.rewrite_cases env c' in + (try trace (str "Pretyping " ++ my_print_constr_expr c) with _ -> ()); let c' = SPretyping.pretype_gen isevars env ([],[]) kind c' in evar_nf isevars c' @@ -200,15 +200,18 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl) | CWfRec r -> - let _ = trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ - Ppconstr.pr_binders bl ++ str " : " ++ - Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ - Ppconstr.pr_constr_expr body) + let n = out_some n in + let _ = + try trace (str "Rewriting fixpoint: " ++ Ppconstr.pr_id recname ++ + Ppconstr.pr_binders bl ++ str " : " ++ + Ppconstr.pr_constr_expr arityc ++ str " := " ++ spc () ++ + Ppconstr.pr_constr_expr body) + with _ -> () in let env', binders_rel = interp_context isevars env0 bl in let after, ((argname, _, argtyp) as arg), before = list_chop_hd n binders_rel in let argid = match argname with Name n -> n | _ -> assert(false) in - let after' = List.map (fun (n, c, t) -> (n, option_app (lift 1) c, lift 1 t)) after in + let after' = List.map (fun (n, c, t) -> (n, option_map (lift 1) c, lift 1 t)) after in let envwf = push_rel_context before env0 in let wf_rel = interp_constr isevars envwf r in let accarg_id = id_of_string ("Acc_" ^ string_of_id argid) in @@ -233,10 +236,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let _ = let pr c = my_print_constr env c in let prr = Printer.pr_rel_context env in - trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ - str "Intern bl" ++ prr intern_bl ++ spc () ++ - str "Extern bl" ++ prr new_bl ++ spc () ++ - str "Intern arity: " ++ pr intern_arity) + try trace (str "Fun bl: " ++ prr fun_bl ++ spc () ++ + str "Intern bl" ++ prr intern_bl ++ spc () ++ + str "Extern bl" ++ prr new_bl ++ spc () ++ + str "Intern arity: " ++ pr intern_arity) + with _ -> () in let impl = if Impargs.is_implicit_args() @@ -279,14 +283,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env0 lrecnames recdef arityl nv in - let nvrec' = Array.map fst nvrec in(* ignore rec order *) + let nvrec' = Array.map (function (Some n,_) -> n | _ -> 0) nvrec in(* ignore rec order *) let declare arrec defrec = let recvec = Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = - trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr env0 (recvec.(i))); + (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ + my_print_constr env0 (recvec.(i))); + with _ -> ()); let ce = { const_entry_body = mkFix ((nvrec',i),recdecls); const_entry_type = Some arrec.(i); @@ -331,20 +336,20 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed let rec collect_evars i acc = if i < recdefs then let (isevars, info, def) = defrec.(i) in - let _ = trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) in + let _ = try trace (str "In solve evars, isevars is: " ++ Evd.pr_evar_defs !isevars) with _ -> () in let def = evar_nf isevars def in let isevars = Evd.undefined_evars !isevars in - let _ = trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) in + let _ = try trace (str "In solve evars, undefined is: " ++ Evd.pr_evar_defs isevars) with _ -> () in let evm = Evd.evars_of isevars in let _, _, typ = arrec.(i) in let id = namerec.(i) in - let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def (Environ.named_context rec_sign) and typ = Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in + let evars_def, evars_typ, evars = Eterm.eterm_term evm def (Some typ) in (*let evars_typ = match evars_typ with Some t -> t | None -> assert(false) in*) (*let fi = id_of_string (string_of_id id ^ "_evars") in*) (*let ce = @@ -357,10 +362,16 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed trace (str (string_of_id fi) ++ str " is defined");*) let evar_sum = if evars = [] then None - else + else ( + (try trace (str "Building evars sum for : "); + List.iter + (fun (n, t) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env0 t)) + evars; + with _ -> ()); let sum = Subtac_utils.build_dependent_sum evars in - trace (str "Evars sum: " ++ my_print_constr env0 (pi1 sum)); - Some sum + (try trace (str "Evars sum: " ++ my_print_constr env0 (snd sum)); + with _ -> ()); + Some sum) in collect_evars (succ i) ((id, evars_def, evar_sum) :: acc) else acc @@ -370,32 +381,34 @@ let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed (* Solve evars then create the definitions *) let real_evars = filter_map (fun (id, kn, sum) -> - match sum with Some (sumg, sumtac, _) -> Some (id, kn, sumg, sumtac) | None -> None) + match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None) defs in Subtac_utils.and_tac real_evars (fun f _ gr -> - let _ = trace (str "Got a proof of: " ++ pr_global gr) in + let _ = trace (str "Got a proof of: " ++ pr_global gr ++ + str "type: " ++ my_print_constr (Global.env ()) (Global.type_of_global gr)) in let constant = match gr with Libnames.ConstRef c -> c | _ -> assert(false) in try (*let value = Environ.constant_value (Global.env ()) constant in*) let pis = f (mkConst constant) in - trace (str "Accessors: " ++ - List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) - pis (mt())); - trace (str "Applied existentials: " ++ - (List.fold_right - (fun (id, kn, sumg, pi) acc -> - let args = Subtac_utils.destruct_ex pi sumg in - my_print_constr env0 (mkApp (kn, Array.of_list args))) - pis (mt ()))); + (try (trace (str "Accessors: " ++ + List.fold_right (fun (_, _, _, c) acc -> my_print_constr env0 c ++ spc () ++ acc) + pis (mt())); + trace (str "Applied existentials: " ++ + (List.fold_right + (fun (id, kn, sumg, pi) acc -> + let args = Subtac_utils.destruct_ex pi sumg in + my_print_constr env0 (mkApp (kn, Array.of_list args))) + pis (mt ())))) + with _ -> ()); let rec aux pis acc = function (id, kn, sum) :: tl -> (match sum with None -> aux pis (kn :: acc) tl - | Some (sumg, _, _) -> + | Some (_, sumg) -> let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in let args = Subtac_utils.destruct_ex pi sumg in let args = |