diff options
author | 2006-06-20 17:59:35 +0000 | |
---|---|---|
committer | 2006-06-20 17:59:35 +0000 | |
commit | 2efdb17f8104227187f21edefa2d72ad61e676b6 (patch) | |
tree | fd50116bc72b81062e3462febc621cd63466be67 | |
parent | 6314b34d1eb8d8614706068020566d776f0a50fb (diff) |
Progress in new wf def typing.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8965 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/subtac/Utils.v | 10 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 52 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 35 |
3 files changed, 89 insertions, 8 deletions
diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index db10cb2a1..b1694d7c2 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -34,3 +34,13 @@ induction t. simpl ; auto. Qed. +Ltac destruct_one_pair := + match goal with + | [H : (ex _) |- _] => destruct H + | [H : (ex2 _) |- _] => destruct H + | [H : (sig _) |- _] => destruct H + | [H : (_ /\ _) |- _] => destruct H +end. + +Ltac destruct_exists := repeat (destruct_one_pair) . + diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 10c5f580b..247336386 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -222,7 +222,7 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed = let projection = mkApp (proj, [| argtyp ; (mkLambda (Name argid', argtyp, - (mkApp (wf_rel, [|mkRel 1; mkRel 2|])))) ; + (mkApp (wf_rel, [|mkRel 1; mkRel 3|])))) ; mkRel 1 |]) in @@ -277,16 +277,54 @@ let build_wellfounded (recname, n, bl,arityc,body) r notation boxed = let fullctyp = Evarutil.nf_isevar !isevars typ in let _ = try trace (str "After evar normalization: " ++ spc () ++ str "Coq term: " ++ my_print_constr env fullcoqc ++ spc () - ++ str "Coq type: " ++ my_print_constr env fullctyp) + ++ str "Coq type: " ++ my_print_constr env fullctyp) with _ -> () in let evm = non_instanciated_map env isevars in let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in - let tac = Eterm.etermtac (evm, fullcoqc) in - trace (str "Starting proof of goal: " ++ my_print_constr env fullctyp); - Command.start_proof recname goal_kind fullctyp (fun _ _ -> ()); - trace (str "Started proof"); - Pfedit.by tac + let evars_def, evars_typ, evars = Eterm.eterm_term evm fullcoqc (Some fullctyp) in + let evars_typ = out_some evars_typ in + let evars_sum = + if evars = [] then None + 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 env t)) + evars; + with _ -> ()); + let sum = Subtac_utils.build_dependent_sum evars in + (try trace (str "Evars sum: " ++ my_print_constr env (snd sum)); + trace (str "Evars type: " ++ my_print_constr env evars_typ); + with _ -> ()); + Some sum) + in + match evars_sum with + | Some (sum_tac, sumg) -> + let proofid = id_of_string (string_of_id recname ^ "_evars_proof") in + Command.start_proof proofid goal_kind sumg + (fun _ gr -> + let constant = match gr with Libnames.ConstRef c -> c + | _ -> assert(false) + in + let def = mkConst constant in + let args = Subtac_utils.destruct_ex def sumg in + let args = + List.map (fun c -> + try Reductionops.whd_betadeltaiota (Global.env ()) Evd.empty c + with Not_found -> + trace (str "Not_found while reducing " ++ + my_print_constr (Global.env ()) c); + c + ) args + in + let _, newdef = decompose_lam_n (List.length args) evars_def in + let constr = Term.substl (List.rev args) newdef in + debug 1 (str "Applied existentials : " ++ my_print_constr env constr)); + trace (str "Started existentials proof"); + Pfedit.by sum_tac; + trace (str "Applied sum tac") + | None -> () + let build_mutrec l boxed = let sigma = Evd.empty diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index 31fea63d5..0d3ebe186 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -167,7 +167,7 @@ let build_dependent_sum l = (n, t) :: tl -> let t' = mkLambda (Name n, t, typ) in trace (spc () ++ str ("treating evar " ^ string_of_id n)); - (try trace (str " assert: " ++ my_print_constr (Global.env ()) t) + (try trace (str " assert: " ++ my_print_constr (Global.env ()) t) with _ -> ()); let tac' = tclTHENS (assert_tac true (Name n) t) @@ -186,6 +186,39 @@ let build_dependent_sum l = (_, hd) :: tl -> aux (intros, hd) tl | [] -> raise (Invalid_argument "build_dependent_sum") +let id x = x + +let build_dependent_sum l = + let rec aux names conttac conttype = function + (n, t) :: ((_ :: _) as tl) -> + let hyptype = substl names t in + trace (spc () ++ str ("treating evar " ^ string_of_id n)); + (try trace (str " assert: " ++ my_print_constr (Global.env ()) hyptype) + with _ -> ()); + let tac = assert_tac true (Name n) hyptype in + let conttac = + (fun cont -> + conttac + (tclTHENS tac + ([intros; + (tclTHENSEQ + [constructor_tac (Some 1) 1 + (Rawterm.ImplicitBindings [mkVar n]); + cont]); + ]))) + in + let conttype = + (fun typ -> + let tex = mkLambda (Name n, t, typ) in + conttype + (mkApp (Lazy.force ex_ind, [| t; tex |]))) + in + aux (mkVar n :: names) conttac conttype tl + | (n, t) :: [] -> + (conttac intros, conttype t) + | [] -> raise (Invalid_argument "build_dependent_sum") + in aux [] id id (List.rev l) + open Proof_type open Tacexpr |