1 files changed, 484 insertions, 0 deletions
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
new file mode 100644
index 00000000..06a80f68
--- /dev/null
+++ b/plugins/subtac/subtac_utils.ml
@@ -0,0 +1,484 @@
+open Evd
+open Libnames
+open Coqlib
+open Term
+open Names
+open Util
+
+let ($) f x = f x
+
+(****************************************************************************)
+(* Library linking *)
+
+let contrib_name = "Program"
+
+let subtac_dir = [contrib_name]
+let fix_sub_module = "Wf"
+let utils_module = "Utils"
+let fixsub_module = subtac_dir @ [fix_sub_module]
+let utils_module = subtac_dir @ [utils_module]
+let tactics_module = subtac_dir @ ["Tactics"]
+let init_constant dir s = gen_constant contrib_name dir s
+let init_reference dir s = gen_reference contrib_name dir s
+
+let fixsub = lazy (init_constant fixsub_module "Fix_sub")
+let ex_pi1 = lazy (init_constant utils_module "ex_pi1")
+let ex_pi2 = lazy (init_constant utils_module "ex_pi2")
+
+let make_ref l s = lazy (init_reference l s)
+let well_founded_ref = make_ref ["Init";"Wf"] "Well_founded"
+let acc_ref = make_ref  ["Init";"Wf"] "Acc"
+let acc_inv_ref = make_ref  ["Init";"Wf"] "Acc_inv"
+let fix_sub_ref = make_ref fixsub_module "Fix_sub"
+let measure_on_R_ref = make_ref fixsub_module "MR"
+let fix_measure_sub_ref = make_ref fixsub_module "Fix_measure_sub"
+let refl_ref = make_ref ["Init";"Logic"] "refl_equal"
+
+let make_ref s = Qualid (dummy_loc, qualid_of_string s)
+let lt_ref = make_ref "Init.Peano.lt"
+let sig_ref = make_ref "Init.Specif.sig"
+let proj1_sig_ref = make_ref "Init.Specif.proj1_sig"
+let proj2_sig_ref = make_ref "Init.Specif.proj2_sig"
+
+let build_sig () =
+  { proj1 = init_constant ["Init"; "Specif"] "proj1_sig";
+    proj2 = init_constant ["Init"; "Specif"] "proj2_sig";
+    elim = init_constant ["Init"; "Specif"] "sig_rec";
+    intro = init_constant ["Init"; "Specif"] "exist";
+    typ = init_constant ["Init"; "Specif"] "sig" }
+
+let sig_ = lazy (build_sig ())
+
+let fix_proto = lazy (init_constant tactics_module "fix_proto")
+let fix_proto_ref () = 
+  match Nametab.global (make_ref "Program.Tactics.fix_proto") with
+  | ConstRef c -> c
+  | _ -> assert false
+
+let eq_ind = lazy (init_constant ["Init"; "Logic"] "eq")
+let eq_rec = lazy (init_constant ["Init"; "Logic"] "eq_rec")
+let eq_rect = lazy (init_constant ["Init"; "Logic"] "eq_rect")
+let eq_refl = lazy (init_constant ["Init"; "Logic"] "refl_equal")
+let eq_ind_ref = lazy (init_reference ["Init"; "Logic"] "eq")
+let refl_equal_ref = lazy (init_reference ["Init"; "Logic"] "refl_equal")
+
+let not_ref = lazy (init_constant ["Init"; "Logic"] "not")
+
+let and_typ = lazy (Coqlib.build_coq_and ())
+
+let eqdep_ind = lazy (init_constant [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_rec = lazy (init_constant ["Logic";"Eqdep"] "eq_dep_rec")
+let eqdep_ind_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep")
+let eqdep_intro_ref = lazy (init_reference [ "Logic";"Eqdep"] "eq_dep_intro")
+
+let jmeq_ind =
+  lazy (check_required_library ["Coq";"Logic";"JMeq"];
+	init_constant ["Logic";"JMeq"] "JMeq")
+let jmeq_rec =
+  lazy (check_required_library ["Coq";"Logic";"JMeq"];
+	init_constant ["Logic";"JMeq"] "JMeq_rec")
+let jmeq_refl =
+  lazy (check_required_library ["Coq";"Logic";"JMeq"];
+	init_constant ["Logic";"JMeq"] "JMeq_refl")
+
+let ex_ind = lazy (init_constant ["Init"; "Logic"] "ex")
+let ex_intro = lazy (init_reference ["Init"; "Logic"] "ex_intro")
+
+let proj1 = lazy (init_constant ["Init"; "Logic"] "proj1")
+let proj2 = lazy (init_constant ["Init"; "Logic"] "proj2")
+
+let boolind = lazy (init_constant ["Init"; "Datatypes"] "bool")
+let sumboolind = lazy (init_constant ["Init"; "Specif"] "sumbool")
+let natind = lazy (init_constant ["Init"; "Datatypes"] "nat")
+let intind = lazy (init_constant ["ZArith"; "binint"] "Z")
+let existSind = lazy (init_constant ["Init"; "Specif"] "sigS")
+
+let existS = lazy (build_sigma_type ())
+
+let prod = lazy (build_prod ())
+
+
+(* orders *)
+let well_founded = lazy (init_constant ["Init"; "Wf"] "well_founded")
+let fix = lazy (init_constant ["Init"; "Wf"] "Fix")
+let acc = lazy (init_constant ["Init"; "Wf"] "Acc")
+let acc_inv = lazy (init_constant ["Init"; "Wf"] "Acc_inv")
+
+let extconstr = Constrextern.extern_constr true (Global.env ())
+let extsort s = Constrextern.extern_constr true (Global.env ()) (mkSort s)
+
+open Pp
+
+let my_print_constr = Termops.print_constr_env
+let my_print_constr_expr = Ppconstr.pr_constr_expr
+let my_print_rel_context env ctx = Printer.pr_rel_context env ctx
+let my_print_context = Termops.print_rel_context
+let my_print_named_context = Termops.print_named_context
+let my_print_env = Termops.print_env
+let my_print_rawconstr = Printer.pr_rawconstr_env
+let my_print_evardefs = Evd.pr_evar_map
+
+let my_print_tycon_type = Evarutil.pr_tycon_type
+
+let debug_level = 2
+
+let debug_on = true
+
+let debug n s =
+  if debug_on then
+    if !Flags.debug && n >= debug_level then
+      msgnl s
+    else ()
+  else ()
+
+let debug_msg n s =
+  if debug_on then
+    if !Flags.debug  && n >= debug_level then s
+    else mt ()
+  else mt ()
+
+let trace s =
+  if debug_on then
+    if !Flags.debug  && debug_level > 0 then msgnl s
+    else ()
+  else ()
+
+let rec pp_list f = function
+    [] -> mt()
+  | x :: y -> f x ++ spc () ++ pp_list f y
+
+let wf_relations = Hashtbl.create 10
+
+let std_relations () =
+  let add k v = Hashtbl.add wf_relations k v in
+    add (init_constant ["Init"; "Peano"] "lt")
+      (lazy (init_constant ["Arith"; "Wf_nat"] "lt_wf"))
+
+let std_relations = Lazy.lazy_from_fun std_relations
+
+type binders = Topconstr.local_binder list
+
+let app_opt c e =
+  match c with
+      Some constr -> constr e
+    | None -> e
+
+let print_args env args =
+  Array.fold_right (fun a acc -> my_print_constr env a ++ spc () ++ acc) args (str "")
+
+let make_existential loc ?(opaque = Define true) env isevars c =
+  let evar = Evarutil.e_new_evar isevars env ~src:(loc, QuestionMark opaque) c in
+  let (key, args) = destEvar evar in
+    (try trace (str "Constructed evar " ++ int key ++ str " applied to args: " ++
+		  print_args env args ++ str " for type: "++
+		  my_print_constr env c) with _ -> ());
+    evar
+
+let make_existential_expr loc env c =
+  let key = Evarutil.new_untyped_evar () in
+  let evar = Topconstr.CEvar (loc, key, None) in
+    debug 2 (str "Constructed evar " ++ int key);
+    evar
+
+let string_of_hole_kind = function
+  | ImplicitArg _ -> "ImplicitArg"
+  | BinderType _ -> "BinderType"
+  | QuestionMark _ -> "QuestionMark"
+  | CasesType -> "CasesType"
+  | InternalHole -> "InternalHole"
+  | TomatchTypeParameter _ -> "TomatchTypeParameter"
+  | GoalEvar -> "GoalEvar"
+  | ImpossibleCase -> "ImpossibleCase"
+  | MatchingVar _ -> "MatchingVar"
+
+let evars_of_term evc init c =
+  let rec evrec acc c =
+    match kind_of_term c with
+    | Evar (n, _) when Evd.mem evc n -> Evd.add acc n (Evd.find evc n)
+    | Evar (n, _) -> assert(false)
+    | _ -> fold_constr evrec acc c
+  in
+    evrec init c
+
+let non_instanciated_map env evd evm =
+  List.fold_left
+    (fun evm (key, evi) ->
+       let (loc,k) = evar_source key !evd in
+	 debug 2 (str "evar " ++ int key ++ str " has kind " ++
+		    str (string_of_hole_kind k));
+	 match k with
+	 | QuestionMark _ -> Evd.add evm key evi
+	 | ImplicitArg (_,_,false) -> Evd.add evm key evi
+	 | _ ->
+	     debug 2 (str " and is an implicit");
+	     Pretype_errors.error_unsolvable_implicit loc env evm (Evarutil.nf_evar_info evm evi) k None)
+    Evd.empty (Evarutil.non_instantiated evm)
+
+let global_kind = Decl_kinds.IsDefinition Decl_kinds.Definition
+let goal_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Definition
+
+let global_proof_kind = Decl_kinds.IsProof Decl_kinds.Lemma
+let goal_proof_kind = Decl_kinds.Global, Decl_kinds.Proof Decl_kinds.Lemma
+
+let global_fix_kind = Decl_kinds.IsDefinition Decl_kinds.Fixpoint
+let goal_fix_kind = Decl_kinds.Global, Decl_kinds.DefinitionBody Decl_kinds.Fixpoint
+
+open Tactics
+open Tacticals
+
+let id x = x
+let filter_map f l =
+  let rec aux acc = function
+      hd :: tl -> (match f hd with Some t -> aux (t :: acc) tl
+		     | None -> aux acc tl)
+    | [] -> List.rev acc
+  in aux [] l
+
+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 (Name n) hyptype in
+	let conttac =
+	  (fun cont ->
+	     conttac
+	     (tclTHENS tac
+		([intros;
+		  (tclTHENSEQ
+		     [constructor_tac false (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
+
+let mkProj1 a b c =
+  mkApp (Lazy.force proj1, [| a; b; c |])
+
+let mkProj2 a b c =
+  mkApp (Lazy.force proj2, [| a; b; c |])
+
+let mk_ex_pi1 a b c =
+  mkApp (Lazy.force ex_pi1, [| a; b; c |])
+
+let mk_ex_pi2 a b c =
+  mkApp (Lazy.force ex_pi2, [| a; b; c |])
+
+let mkSubset name typ prop =
+  mkApp ((Lazy.force sig_).typ,
+	 [| typ; mkLambda (name, typ, prop) |])
+
+let mk_eq typ x y = mkApp (Lazy.force eq_ind, [| typ; x ; y |])
+let mk_eq_refl typ x = mkApp (Lazy.force eq_refl, [| typ; x |])
+let mk_JMeq typ x typ' y = mkApp (Lazy.force jmeq_ind, [| typ; x ; typ'; y |])
+let mk_JMeq_refl typ x = mkApp (Lazy.force jmeq_refl, [| typ; x |])
+
+let unsafe_fold_right f = function
+    hd :: tl -> List.fold_right f tl hd
+  | [] -> raise (Invalid_argument "unsafe_fold_right")
+
+let mk_conj l =
+  let conj_typ = Lazy.force and_typ in
+    unsafe_fold_right
+      (fun c conj ->
+	 mkApp (conj_typ, [| c ; conj |]))
+      l
+
+let mk_not c =
+  let notc = Lazy.force not_ref in
+    mkApp (notc, [| c |])
+
+let and_tac l hook =
+  let andc = Coqlib.build_coq_and () in
+  let rec aux ((accid, goal, tac, extract) as acc) = function
+    | [] -> (* Singleton *) acc
+
+    | (id, x, elgoal, eltac) :: tl ->
+	let tac' = tclTHEN simplest_split (tclTHENLIST [tac; eltac]) in
+	let proj = fun c -> mkProj2 goal elgoal c in
+	let extract = List.map (fun (id, x, y, f) -> (id, x, y, (fun c -> f (mkProj1 goal elgoal c)))) extract in
+	  aux ((string_of_id id) ^ "_" ^ accid, mkApp (andc, [| goal; elgoal |]), tac',
+	       (id, x, elgoal, proj) :: extract) tl
+
+  in
+  let and_proof_id, and_goal, and_tac, and_extract =
+    match l with
+      | [] -> raise (Invalid_argument "and_tac: empty list of goals")
+      | (hdid, x, hdg, hdt) :: tl ->
+	  aux (string_of_id hdid, hdg, hdt, [hdid, x, hdg, (fun c -> c)]) tl
+  in
+  let and_proofid = id_of_string (and_proof_id ^ "_and_proof") in
+    Lemmas.start_proof and_proofid goal_kind and_goal
+      (hook (fun c -> List.map (fun (id, x, t, f) -> (id, x, t, f c)) and_extract));
+    trace (str "Started and proof");
+    Pfedit.by and_tac;
+    trace (str "Applied and tac")
+
+
+let destruct_ex ext ex =
+  let rec aux c acc =
+    match kind_of_term c with
+	App (f, args) ->
+	  (match kind_of_term f with
+	       Ind i when i = Term.destInd (Lazy.force ex_ind) && Array.length args = 2 ->
+		 let (dom, rng) =
+		   try (args.(0), args.(1))
+		   with _ -> assert(false)
+		 in
+		 let pi1 = (mk_ex_pi1 dom rng acc) in
+		 let rng_body =
+		   match kind_of_term rng with
+		       Lambda (_, _, t) -> subst1 pi1 t
+		     | t -> rng
+		 in
+		   pi1 :: aux rng_body (mk_ex_pi2 dom rng acc)
+	     | _ -> [acc])
+      | _ -> [acc]
+  in aux ex ext
+
+open Rawterm
+
+let id_of_name = function
+    Name n -> n
+  | Anonymous -> raise (Invalid_argument "id_of_name")
+
+let definition_message id =
+  Nameops.pr_id id ++ str " is defined"
+
+let recursive_message v =
+  match Array.length v with
+    | 0 -> error "no recursive definition"
+    | 1 -> (Printer.pr_constant (Global.env ()) v.(0) ++ str " is recursively defined")
+    | _ -> hov 0 (prvect_with_sep pr_comma (Printer.pr_constant (Global.env ())) v ++
+		    spc () ++ str "are recursively defined")
+
+let print_message m =
+  Flags.if_verbose ppnl m
+
+(* Solve an obligation using tactics, return the corresponding proof term *)
+let solve_by_tac evi t =
+  let id = id_of_string "H" in
+  try
+    Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl
+    (fun _ _ -> ());
+    Pfedit.by (tclCOMPLETE t);
+    let _,(const,_,_,_) = Pfedit.cook_proof ignore in
+      Pfedit.delete_current_proof (); 
+      Inductiveops.control_only_guard (Global.env ())
+	const.Entries.const_entry_body;
+      const.Entries.const_entry_body
+  with e ->
+    Pfedit.delete_current_proof();
+    raise e
+
+(* let apply_tac t goal = t goal *)
+
+(* let solve_by_tac evi t = *)
+(*   let ev = 1 in *)
+(*   let evm = Evd.add Evd.empty ev evi in *)
+(*   let goal = {it = evi; sigma = evm } in *)
+(*   let (res, valid) = apply_tac t goal in *)
+(*     if res.it = [] then *)
+(*       let prooftree = valid [] in *)
+(*       let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *)
+(* 	if obls = [] then proofterm *)
+(* 	else raise Exit *)
+(*     else raise Exit *)
+
+let rec string_of_list sep f = function
+    [] -> ""
+  | x :: [] -> f x
+  | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl
+
+let string_of_intset d =
+  string_of_list "," string_of_int (Intset.elements d)
+
+(**********************************************************)
+(* Pretty-printing *)
+open Printer
+open Ppconstr
+open Nameops
+open Termops
+open Evd
+
+let pr_meta_map evd =
+  let ml = meta_list evd in
+  let pr_name = function
+      Name id -> str"[" ++ pr_id id ++ str"]"
+    | _ -> mt() in
+  let pr_meta_binding = function
+    | (mv,Cltyp (na,b)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " : " ++
+           print_constr b.rebus ++ fnl ())
+    | (mv,Clval(na,b,_)) ->
+      	hov 0
+	  (pr_meta mv ++ pr_name na ++ str " := " ++
+             print_constr (fst b).rebus ++ fnl ())
+  in
+  prlist pr_meta_binding ml
+
+let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+
+let pr_evar_info evi =
+  let phyps =
+    (*pr_idl (List.rev (ids_of_named_context (evar_context evi))) *)
+    Printer.pr_named_context (Global.env()) (evar_context evi)
+  in
+  let pty = print_constr evi.evar_concl in
+  let pb =
+    match evi.evar_body with
+      | Evar_empty -> mt ()
+      | Evar_defined c -> spc() ++ str"=> "  ++ print_constr c
+  in
+  hov 2 (str"["  ++ phyps ++ spc () ++ str"|- "  ++ pty ++ pb ++ str"]")
+
+let pr_evar_map sigma =
+  h 0
+    (prlist_with_sep pr_fnl
+      (fun (ev,evi) ->
+        h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi))
+      (to_list sigma))
+
+let pr_constraints pbs =
+  h 0
+    (prlist_with_sep pr_fnl (fun (pbty,t1,t2) ->
+      print_constr t1 ++ spc() ++
+      str (match pbty with
+	| Reduction.CONV -> "=="
+	| Reduction.CUMUL -> "<=") ++
+      spc() ++ print_constr t2) pbs)
+
+let pr_evar_map evd =
+  let pp_evm =
+    let evars =  evd in
+    if evars = empty then mt() else
+      str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in
+  let pp_met =
+    if meta_list evd = [] then mt() else
+      str"METAS:"++brk(0,1)++pr_meta_map evd in
+  v 0 (pp_evm ++ pp_met)
+
+let contrib_tactics_path =
+  make_dirpath (List.map id_of_string ["Tactics";contrib_name;"Coq"])
+let tactics_tac s =
+  lazy(make_kn (MPfile contrib_tactics_path) (make_dirpath []) (mk_label s))
+
+let tactics_call tac args =
+  TacArg(TacCall(dummy_loc, ArgArg(dummy_loc, Lazy.force (tactics_tac tac)),args))