path: root/contrib/subtac/subtac_command.ml

open Closure
open RedFlags
open Declarations
open Entries
open Dyn
open Libobject
open Pattern
open Matching
open Pp
open Rawterm
open Sign
open Tacred
open Util
open Names
open Nameops
open Libnames
open Nametab
open Pfedit
open Proof_type
open Refiner
open Tacmach
open Tactic_debug
open Topconstr
open Term
open Termops
open Tacexpr
open Safe_typing
open Typing
open Hiddentac
open Genarg
open Decl_kinds
open Mod_subst
open Printer
open Inductiveops
open Syntax_def
open Environ
open Tactics
open Tacticals
open Tacinterp
open Vernacexpr
open Notation

module SPretyping = Subtac_pretyping.Pretyping
open Subtac_utils
open Pretyping
open Subtac_obligations

(*********************************************************************)
(* Functions to parse and interpret constructions *)

let evar_nf isevars c =
  isevars := Evarutil.nf_evar_defs !isevars;
  Evarutil.nf_isevar !isevars c

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_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'
    
let interp_constr isevars env c =
  interp_gen (OfType None) isevars env c 

let interp_type isevars env ?(impls=([],[])) c =
  interp_gen IsType isevars env ~impls c

let interp_casted_constr isevars env ?(impls=([],[])) c typ =
  interp_gen (OfType (Some typ)) isevars env ~impls c 

let interp_open_constr isevars env c =
    msgnl (str "Pretyping " ++ my_print_constr_expr c);
  let c = Constrintern.intern_constr (Evd.evars_of !isevars) env c in
  let c' = SPretyping.pretype_gen isevars env ([], []) (OfType None) c in
    evar_nf isevars c'

let interp_constr_judgment isevars env c =
  let j = 
    SPretyping.understand_judgment_tcc isevars env
      (Constrintern.intern_constr (Evd.evars_of !isevars) env c) 
  in
    { uj_val = evar_nf isevars j.uj_val; uj_type = evar_nf isevars j.uj_type }

let locate_if_isevar loc na = function
  | RHole _ -> 
      (try match na with
	| Name id ->  Reserve.find_reserved_type id
	| Anonymous -> raise Not_found 
      with Not_found -> RHole (loc, Evd.BinderType na))
  | x -> x

let interp_binder sigma env na t =
  let t = Constrintern.intern_gen true (Evd.evars_of !sigma) env t in
    SPretyping.understand_type (Evd.evars_of !sigma) env (locate_if_isevar (loc_of_rawconstr t) na t)
      

let interp_context sigma env params = 
  List.fold_left
    (fun (env,params) d -> match d with
      | LocalRawAssum ([_,na],(CHole _ as t)) ->
	  let t = interp_binder sigma env na t in
	  let d = (na,None,t) in
	  (push_rel d env, d::params)
      | LocalRawAssum (nal,t) ->
	  let t = interp_type sigma env t in
	  let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
	  let ctx = List.rev ctx in
	  (push_rel_context ctx env, ctx@params)
      | LocalRawDef ((_,na),c) ->
	  let c = interp_constr_judgment sigma env c in
	  let d = (na, Some c.uj_val, c.uj_type) in
	  (push_rel d env,d::params))
    (env,[]) params

(* try to find non recursive definitions *)

let list_chop_hd i l = match list_chop i l with
  | (l1,x::l2) -> (l1,x,l2)
  | (x :: [], l2) -> ([], x, [])
  | _ -> assert(false)

let collect_non_rec env = 
  let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
    try
      let i = 
        list_try_find_i
          (fun i f ->
             if List.for_all (fun (_, _, def) -> not (occur_var env f def)) ldefrec
             then i else failwith "try_find_i")
          0 lnamerec 
      in
      let (lf1,f,lf2) = list_chop_hd i lnamerec in
      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
      let (lar1,ar,lar2) = list_chop_hd i larrec in
      let newlnv = 
	try 
	  match list_chop i nrec with 
            | (lnv1,_::lnv2) -> (lnv1@lnv2)
	    | _ -> [] (* nrec=[] for cofixpoints *)
        with Failure "list_chop" -> []
      in 
      searchrec ((f,def,ar)::lnonrec) 
	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
    with Failure "try_find_i" -> 
      (List.rev lnonrec,
       (Array.of_list lnamerec, Array.of_list ldefrec,
        Array.of_list larrec, Array.of_list nrec))
  in 
  searchrec [] 


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 list_of_local_binders l = 
  let rec aux acc = function
      Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl
    | Topconstr.LocalRawAssum (nl, c) :: tl -> 
	aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl
    | [] -> List.rev acc
  in aux [] l

let lift_binders k n l =
  let rec aux n = function
    | (id, t, c) :: tl -> (id, option_map (liftn k n) t, liftn k n c) :: aux (pred n) tl
    | [] -> []
  in aux n l

let rec gen_rels = function
    0 -> []
  | n -> mkRel n :: gen_rels (pred n)

let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
  let sigma = Evd.empty in
  let isevars = ref (Evd.create_evar_defs sigma) in
  let env = Global.env() in 
  let pr c = my_print_constr env c in
  let prr = Printer.pr_rel_context env in
  let prn = Printer.pr_named_context env in
  let pr_rel env = Printer.pr_rel_context env in
  let nc = named_context env in
  let nc_len = named_context_length nc in
  let _ = 
    try debug 2 (str "In named context: " ++ prn (named_context env) ++ 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 env bl in
  let after, ((argname, _, argtyp) as arg), before = list_chop_hd (succ n) binders_rel in
  let before_length, after_length = List.length before, List.length after in
  let argid = match argname with Name n -> n | _ -> assert(false) in
  let _liftafter = lift_binders 1 after_length after in
  let envwf = push_rel_context before env in
  let wf_rel, wf_rel_fun, measure_fn = 
    let rconstr_body, rconstr = 
      let app = mkAppC (r, [mkIdentC (id_of_name argname)]) in
       let env = push_rel_context [arg] envwf in
       let capp = interp_constr isevars env app in
 	capp, mkLambda (argname, argtyp, capp)
     in
       if measure then
 	let lt_rel = constr_of_global (Lazy.force lt_ref) in
 	let name s = Name (id_of_string s) in
 	let wf_rel_fun = 
 	  (fun x y ->
 	      mkApp (lt_rel, [| subst1 x rconstr_body; 
 				subst1 y rconstr_body |])) 
 	in
 	let wf_rel = 
 	  mkLambda (name "x", argtyp,
 		    mkLambda (name "y", lift 1 argtyp,
 			      wf_rel_fun (mkRel 2) (mkRel 1)))
 	in
 	  wf_rel, wf_rel_fun , Some rconstr
       else rconstr, (fun x y -> mkApp (rconstr, [|x; y|])), None
  in
  let wf_proof = mkApp (Lazy.force well_founded, [| argtyp ; wf_rel |])
  in
  let argid' = id_of_string (string_of_id argid ^ "'") in
  let wfarg len = (Name argid', None, 
  		   mkSubset (Name argid') argtyp 
		     (wf_rel_fun (mkRel 1) (mkRel (len + 1))))
  in
  let top_bl = after @ (arg :: before) in
  let intern_bl = after @ (wfarg 1 :: arg :: before) in
  let top_env = push_rel_context top_bl env in
  let intern_env = push_rel_context intern_bl env in
  let top_arity = interp_type isevars top_env arityc in
  (try debug 2 (str "Intern bl: " ++ prr intern_bl) with _ -> ());
  let proj = (Lazy.force sig_).Coqlib.proj1 in
  let projection = 
    mkApp (proj, [| argtyp ;
		    (mkLambda (Name argid', argtyp,
			       (wf_rel_fun (mkRel 1) (mkRel 3)))) ;
		    mkRel 1
		 |])
  in
  (try debug 2 (str "Top arity: " ++ my_print_constr top_env top_arity) with _ -> ());
  let intern_arity = substnl [projection] after_length top_arity in 
  (try debug 2 (str "Top arity after subst: " ++ my_print_constr intern_env intern_arity) with _ -> ());
  let intern_before_env = push_rel_context before env in
  let intern_fun_bl = after @ [wfarg 1]  in
  (try debug 2 (str "Intern fun bl: " ++ prr intern_fun_bl) with _ -> ());
  let intern_fun_arity = intern_arity in
  (try debug 2 (str "Intern fun arity: " ++ 
		  my_print_constr intern_env intern_fun_arity) with _ -> ());
  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_fun_arity intern_fun_bl in
  let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
  let fun_bl = after @ (intern_fun_binder :: [arg]) in
  (try debug 2 (str "Fun bl: " ++ pr_rel intern_before_env fun_bl ++ spc ()) with _ -> ());
  let fun_env = push_rel_context fun_bl intern_before_env in
  let fun_arity = interp_type isevars fun_env arityc in
  let intern_body = interp_casted_constr isevars fun_env body fun_arity in
  let intern_body_lam = it_mkLambda_or_LetIn intern_body fun_bl in
  let _ = 
      try debug 2 (str "Fun bl: " ++ prr fun_bl ++ spc () ++
		   str "Intern bl" ++ prr intern_bl ++ spc () ++
		   str "Top bl" ++ prr top_bl ++ spc () ++
		   str "Intern arity: " ++ pr intern_arity ++
		   str "Top arity: " ++ pr top_arity ++ spc () ++
		   str "Intern body " ++ pr intern_body_lam)
      with _ -> ()
  in
  let _impl = 
    if Impargs.is_implicit_args()
    then Impargs.compute_implicits top_env top_arity
    else [] 
  in
  let prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
  let fix_def =
    match measure_fn with
	None ->
	  mkApp (constr_of_reference (Lazy.force fix_sub_ref), 
		 [| argtyp ;
		    wf_rel ;
		    make_existential dummy_loc intern_before_env isevars wf_proof ;
		    prop ;
		    intern_body_lam |])
      | Some f ->
	  mkApp (constr_of_reference (Lazy.force fix_measure_sub_ref), 
		 [| argtyp ; f ; prop ;
		    intern_body_lam |])
  in
  let def_appl = applist (fix_def, gen_rels (after_length + 1)) in
  let def = it_mkLambda_or_LetIn def_appl binders_rel in
  let typ = it_mkProd_or_LetIn top_arity binders_rel in
    debug 2 (str "Constructed def");
    debug 2 (my_print_constr intern_before_env def);
    debug 2 (str "Type: " ++ my_print_constr env typ);
  let fullcoqc = Evarutil.nf_isevar !isevars def in
  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) 
     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 evars, evars_def = Eterm.eterm_obligations recname nc_len evm fullcoqc (Some fullctyp) in
    (try trace (str "Generated obligations : ");
       Array.iter
	 (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t))
	 evars;
     with _ -> ());    
      trace (str "Adding to obligations list");
      Subtac_obligations.add_entry recname evars_def fullctyp evars;
      trace (str "Added to obligations list")
(*
let build_mutrec l boxed = 
  let sigma = Evd.empty
  and env0 = Global.env()
  in 
  let lnameargsardef =
    (*List.map (fun (f, d) -> Subtac_interp_fixpoint.rewrite_fixpoint env0 protos (f, d))*)
    l
  in
  let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
  and nv = List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef
  in
    (* Build the recursive context and notations for the recursive types *)
  let (rec_sign,rec_impls,arityl) = 
    List.fold_left 
      (fun (env,impls,arl) ((recname, n, bl,arityc,body),_) -> 
	 let isevars = ref (Evd.create_evar_defs sigma) in	  
	 let arityc = Command.generalize_constr_expr arityc bl in
	 let arity = interp_type isevars env0 arityc in
	 let impl = 
	   if Impargs.is_implicit_args()
	   then Impargs.compute_implicits env0 arity
	   else [] in
	 let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
	   (Environ.push_named (recname,None,arity) env, impls', (isevars, None, arity)::arl))
      (env0,[],[]) lnameargsardef in
  let arityl = List.rev arityl in
  let notations = 
    List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
      lnameargsardef [] in

  let recdef =

    (* Declare local notations *)
    let fs = States.freeze() in
    let def = 
      try
	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
	List.map2
	  (fun ((_,_,bl,_,def),_) (isevars, info, arity) ->
	     match info with
		 None ->
		   let def = abstract_constr_expr def bl in
		     isevars, info, interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
		       def arity
	       | Some (n, artyp, wfrel, fun_bl, intern_bl, intern_arity) ->
		   let rec_sign = push_rel_context fun_bl rec_sign in
		   let cstr = interp_casted_constr isevars rec_sign ~impls:([],rec_impls)
				def intern_arity
		   in isevars, info, it_mkLambda_or_LetIn cstr fun_bl)
          lnameargsardef arityl
      with e ->
	States.unfreeze fs; raise e in
    States.unfreeze fs; def 
  in

  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
    collect_non_rec env0 lrecnames recdef arityl nv in
  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 =
      (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);
          const_entry_opaque = false;
          const_entry_boxed = boxed} in
      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
      in (ConstRef kn)
    in 
      (* declare the recursive definitions *)
    let lrefrec = Array.mapi declare namerec in
      Options.if_verbose ppnl (recursive_message lrefrec);


      (*(* The others are declared as normal definitions *)
      let var_subst id = (id, Constrintern.global_reference id) in
      let _ = 
	List.fold_left
	  (fun subst (f,def,t) ->
	     let ce = { const_entry_body = replace_vars subst def;
			const_entry_type = Some t;
			const_entry_opaque = false;
			const_entry_boxed = boxed } in
	     let _ =
	       Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition)
	     in
      	       warning ((string_of_id f)^" is non-recursively defined");
      	       (var_subst f) :: subst)
	  (List.map var_subst (Array.to_list namerec))
	  lnonrec 
      in*)
      List.iter (fun (df,c,scope) ->
		   Metasyntax.add_notation_interpretation df [] c scope) notations
  in 
  let declare l = 
    let recvec = Array.of_list l
    and arrec = Array.map pi3 arrec
    in declare arrec recvec
  in
  let recdefs = Array.length defrec in
    trace (int recdefs ++ str " recursive definitions");
    (* Solve remaining evars *)
  let rec collect_evars i acc = 
    if i < recdefs then
      let (isevars, info, def) = defrec.(i) 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 _ = 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
      (* 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 = 
	{ const_entry_body = evars_def; 
	  const_entry_type = Some evars_typ;
	  const_entry_opaque = false;
	  const_entry_boxed = boxed} in
      let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Definition) in
	definition_message fi;
	trace (str (string_of_id fi) ++ str " is defined");*)
	let evar_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 env0 t))
		 evars;
	     with _ -> ());
	    let sum = Subtac_utils.build_dependent_sum evars in
	      (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
  in 
  let defs = collect_evars 0 [] in

  (* Solve evars then create the definitions *)
  let real_evars = 
    filter_map (fun (id, kn, sum) ->
		  match sum with Some (sumtac, sumg) -> Some (id, kn, sumg, sumtac) | None -> None)
      defs
  in
    match real_evars with
	[] -> declare (List.rev_map (fun (id, c, _) ->
				   snd (decompose_lam_n recdefs c)) defs)
      | l ->

    Subtac_utils.and_tac real_evars
      (fun f _ gr ->
	 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
	       (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) -> 
			    let (id, kn, sumg, pi), pis = List.hd pis, List.tl pis in
			    let args = Subtac_utils.destruct_ex pi 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 (recdefs + List.length args) kn in
			    let constr = Term.substl (mkRel 1 :: List.rev args) newdef in
			      aux pis (constr :: acc) tl)
		 | [] -> List.rev acc
	       in
		 declare (aux pis [] defs)
	   with Environ.NotEvaluableConst cer ->
	     match cer with
		 Environ.NoBody -> trace (str "Constant has no body")
	       | Environ.Opaque -> trace (str "Constant is opaque")
      )
*)
let out_n = function
    Some n -> n
  | None -> 0

let build_recursive (lnameargsardef:(fixpoint_expr * decl_notation) list) boxed =
  match lnameargsardef with
    | ((id, (n, CWfRec r), bl, typ, body), no) :: [] -> 
	build_wellfounded (id, out_n n, bl, typ, body) r false no boxed
    | ((id, (n, CMeasureRec r), bl, typ, body), no) :: [] -> 
	build_wellfounded (id, out_n n, bl, typ, body) r true no boxed
    | l -> 
	let lnameargsardef = 
	  List.map (fun ((id, (n, ro), bl, typ, body), no) ->
		 match ro with
		     CStructRec -> (id, out_n n, bl, typ, body), no
		   | CWfRec _ | CMeasureRec _ -> 
		       errorlabstrm "Subtac_command.build_recursive"
			 (str "Well-founded fixpoints not allowed in mutually recursive blocks"))
	    lnameargsardef
	in assert(false)
	     (*build_mutrec lnameargsardef boxed*)