1 files changed, 466 insertions, 0 deletions

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
new file mode 100644
index 000000000..674805962
--- /dev/null
+++ b/plugins/subtac/subtac_command.ml
@@ -0,0 +1,466 @@
+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
+open Evd
+open Evarutil
+
+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_patvar=false) ?(ltacvars=([],[]))
+               c =
+  let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in
+  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_evars 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_casted_constr_evars 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 ( !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 ( !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 ( !sigma) env t in
+    SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
+
+let interp_context_evars evdref env params = 
+  let bl = Constrintern.intern_context false ( !evdref) env params in
+  let (env, par, _, impls) =
+    List.fold_left
+      (fun (env,params,n,impls) (na, k, b, t) ->
+	match b with
+	    None ->
+	      let t' = locate_if_isevar (loc_of_rawconstr t) na t in
+	      let t = SPretyping.understand_tcc_evars evdref env IsType t' in
+	      let d = (na,None,t) in
+	      let impls = 
+		if k = Implicit then
+		  let na = match na with Name n -> Some n | Anonymous -> None in
+		    (ExplByPos (n, na), (true, true)) :: impls
+		else impls
+	      in
+		(push_rel d env, d::params, succ n, impls)
+	  | Some b ->
+	      let c = SPretyping.understand_judgment_tcc evdref env b in
+	      let d = (na, Some c.uj_val, c.uj_type) in
+		(push_rel d env,d::params, succ n, impls))
+      (env,[],1,[]) (List.rev bl)
+  in (env, par), impls
+
+(* 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 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, k, 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 split_args n rel = match list_chop ((List.length rel) - n) rel with
+    (l1, x :: l2) -> l1, x, l2
+  | _ -> assert(false)
+
+let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed =
+  Coqlib.check_required_library ["Coq";"Program";"Wf"];
+  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 _ =  *)
+(*     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), impls = interp_context_evars isevars env bl in
+  let after, ((argname, _, argtyp) as arg), before = 
+    let idx = list_index (Name (snd n)) (List.rev_map (fun (na, _, _) -> na) binders_rel) in
+      split_args idx 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
+      trace (str"rconstr_body: " ++ pr rconstr_body);
+       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 lift x y = (* lift to before_env *)
+	  trace (str"lifter rconstr_body:" ++ pr (liftn lift 2 rconstr_body));
+ 	  mkApp (lt_rel, [| subst1 x (liftn lift 2 rconstr_body); 
+ 			    subst1 y (liftn lift 2 rconstr_body) |])
+	in
+ 	let wf_rel = 
+ 	  mkLambda (name "x", argtyp,
+ 		    mkLambda (name "y", lift 1 argtyp,
+ 			      wf_rel_fun 0 (mkRel 2) (mkRel 1)))
+ 	in
+ 	  wf_rel, wf_rel_fun , Some rconstr
+       else rconstr, (fun lift 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') (lift len argtyp) 
+		     (wf_rel_fun (succ len) (mkRel 1) (mkRel (len + 1))))
+  in
+  let top_bl = after @ (arg :: before) in
+  let top_env = push_rel_context top_bl env in
+  let top_arity = interp_type_evars isevars top_env arityc in
+  let intern_bl = wfarg 1 :: arg :: before in
+  let _intern_env = push_rel_context intern_bl env in
+  let proj = (Lazy.force sig_).Coqlib.proj1 in
+  let projection = 
+    mkApp (proj, [| argtyp ;
+		    (mkLambda (Name argid', argtyp,
+			       (wf_rel_fun 1 (mkRel 1) (mkRel 3)))) ;
+		    mkRel 1
+		 |])
+  in
+  let intern_arity = it_mkProd_or_LetIn top_arity after in
+  (* Intern arity is in top_env = arg :: before *)
+  let intern_arity = liftn 2 2 intern_arity in
+(*     trace (str "After lifting arity: " ++  *)
+(* 	      my_print_constr (push_rel (Name argid', None, lift 2 argtyp) intern_env) *)
+(* 	      intern_arity); *)
+  (* arity is now in something :: wfarg :: arg :: before 
+     where what refered to arg now refers to something *)
+  let intern_arity = substl [projection] intern_arity in
+  (* substitute the projection of wfarg for something *)
+  let intern_before_env = push_rel_context before env in
+  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfarg 1] in
+  let intern_fun_binder = (Name recname, None, intern_fun_arity_prod) in
+  let fun_bl = liftafter @ (intern_fun_binder :: [arg]) in
+  let fun_env = push_rel_context fun_bl intern_before_env in
+  let fun_arity = interp_type_evars 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 trace ((* 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 prop = mkLambda (Name argid, argtyp, it_mkProd_or_LetIn top_arity after) in
+    (* Lift to get to constant arguments *)
+  let lift_cst = List.length after + 1 in
+  let fix_def =
+    match measure_fn with
+	None ->
+	  mkApp (constr_of_global (Lazy.force fix_sub_ref), 
+		 [| argtyp ;
+		    wf_rel ;
+		    make_existential dummy_loc ~opaque:(Define false) env isevars wf_proof ;
+		    lift lift_cst prop ;
+		    lift lift_cst intern_body_lam |])
+      | Some f ->
+	  mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), 
+		[| lift lift_cst argtyp ; 
+		   lift lift_cst f ;
+		   lift lift_cst prop ;
+		   lift lift_cst 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
+  let fullcoqc = Evarutil.nf_isevar !isevars def in
+  let fullctyp = Evarutil.nf_isevar !isevars typ in
+  let evm =evars_of_term ( !isevars) Evd.empty fullctyp in
+  let evm = evars_of_term ( !isevars) evm fullcoqc in
+  let evm = non_instanciated_map env isevars evm in
+  let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in
+    Subtac_obligations.add_definition recname evars_def evars_typ ~implicits:impls evars
+
+let nf_evar_context isevars ctx = 
+  List.map (fun (n, b, t) -> 
+    (n, Option.map (Evarutil.nf_isevar isevars) b, Evarutil.nf_isevar isevars t)) ctx
+    
+let interp_fix_context evdref env fix =
+  interp_context_evars evdref env fix.Command.fix_binders
+
+let interp_fix_ccl evdref (env,_) fix =
+  interp_type_evars evdref env fix.Command.fix_type
+
+let interp_fix_body evdref env_rec impls (_,ctx) fix ccl =
+  let env = push_rel_context ctx env_rec in
+  let body = interp_casted_constr_evars evdref env ~impls fix.Command.fix_body ccl in
+  it_mkLambda_or_LetIn body ctx
+
+let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
+
+let prepare_recursive_declaration fixnames fixtypes fixdefs =
+  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+  let names = List.map (fun id -> Name id) fixnames in
+  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
+
+let rel_index n ctx = 
+  list_index0 (Name n) (List.rev_map pi1 (List.filter (fun x -> pi2 x = None) ctx))
+
+let rec unfold f b =
+  match f b with
+    | Some (x, b') -> x :: unfold f b'
+    | None -> []
+
+let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
+  match n with 
+  | Some (loc, n) -> [rel_index n fixctx]
+  | None -> 
+      (* If recursive argument was not given by user, we try all args.
+	 An earlier approach was to look only for inductive arguments,
+	 but doing it properly involves delta-reduction, and it finally 
+         doesn't seem to worth the effort (except for huge mutual 
+	 fixpoints ?) *)
+      let len = List.length fixctx in
+	unfold (function x when x = len -> None 
+	  | n -> Some (n, succ n)) 0
+
+let push_named_context = List.fold_right push_named
+
+let check_evars env initial_sigma evd c =
+  let sigma =  evd in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (evk,args) ->
+          assert (Evd.mem sigma evk);
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk evd in
+	      (match k with
+	      | QuestionMark _ -> ()
+	      | _ ->
+		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
+		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
+let interp_recursive fixkind l boxed =
+  let env = Global.env() in
+  let fixl, ntnl = List.split l in
+  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
+  let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
+
+  (* Interp arities allowing for unresolved types *)
+  let evdref = ref Evd.empty in
+  let fixctxs, fiximps = List.split (List.map (interp_fix_context evdref env) fixl) in
+  let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in
+  let fixtypes = List.map2 build_fix_type fixctxs fixccls in
+  let rec_sign = 
+    List.fold_left2 (fun env id t -> (id,None,t) :: env)
+      [] fixnames fixtypes
+  in
+  let env_rec = push_named_context rec_sign env in
+
+  (* Get interpretation metadatas *)
+  let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in
+  let notations = List.fold_right Option.List.cons ntnl [] in
+
+  (* Interp bodies with rollback because temp use of notations/implicit *)
+  let fixdefs = 
+    States.with_heavy_rollback (fun () -> 
+      List.iter (Command.declare_interning_data impls) notations;
+      list_map3 (interp_fix_body evdref env_rec impls) fixctxs fixl fixccls)
+      () in
+
+  (* Instantiate evars and check all are resolved *)
+  let evd,_ = Evarconv.consider_remaining_unif_problems env_rec !evdref in
+  let fixdefs = List.map (nf_evar ( evd)) fixdefs in
+  let fixtypes = List.map (nf_evar ( evd)) fixtypes in
+  let rec_sign = nf_named_context_evar ( evd) rec_sign in
+    
+  let recdefs = List.length rec_sign in
+  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+  List.iter (check_evars env Evd.empty evd) fixtypes;
+  Command.check_mutuality env kind (List.combine fixnames fixdefs);
+
+  (* Russell-specific code *)
+
+  (* Get the interesting evars, those that were not instanciated *)
+  let isevars = Evd.undefined_evars evd in
+  let evm =  isevars in
+  (* Solve remaining evars *)
+  let rec collect_evars id def typ imps = 
+      (* Generalize by the recursive prototypes  *)
+    let def = 
+      Termops.it_mkNamedLambda_or_LetIn def rec_sign
+    and typ =
+      Termops.it_mkNamedProd_or_LetIn typ rec_sign
+    in
+    let evm' = Subtac_utils.evars_of_term evm Evd.empty def in
+    let evm' = Subtac_utils.evars_of_term evm evm' typ in
+    let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in
+      (id, def, typ, imps, evars)
+  in 
+  let defs = list_map4 collect_evars fixnames fixdefs fixtypes fiximps in
+    (match fixkind with
+      | Command.IsFixpoint wfl ->
+	  let possible_indexes =
+	    list_map3 compute_possible_guardness_evidences wfl fixctxs fixtypes in
+	  let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames), 
+	    Array.of_list fixtypes, 
+	    Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
+	  in
+	  let indexes = Pretyping.search_guard dummy_loc (Global.env ()) possible_indexes fixdecls in
+	    list_iter_i (fun i _ -> Inductive.check_fix env ((indexes,i),fixdecls)) l
+      | Command.IsCoFixpoint -> ());
+    Subtac_obligations.add_mutual_definitions defs notations fixkind
+
+let out_n = function
+    Some n -> n
+  | None -> raise Not_found
+
+let build_recursive l b =
+  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+    match g, l with
+	[(n, CWfRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r false ntn false)
+
+      | [(n, CMeasureRec r)], [(((_,id),_,bl,typ,def),ntn)] ->
+	  ignore(build_wellfounded (id, out_n n, bl, typ, def) r true ntn false)
+
+      | _, _ when List.for_all (fun (n, ro) -> ro = CStructRec) g ->
+	  let fixl = List.map (fun (((_,id),_,bl,typ,def),ntn) -> 
+	    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn)) l 
+	  in interp_recursive (Command.IsFixpoint g) fixl b
+      | _, _ -> 
+	  errorlabstrm "Subtac_command.build_recursive"
+	    (str "Well-founded fixpoints not allowed in mutually recursive blocks")
+
+let build_corecursive l b =
+  let fixl = List.map (fun (((_,id),bl,typ,def),ntn) -> 
+    ({Command.fix_name = id; Command.fix_binders = bl; Command.fix_body = def; Command.fix_type = typ},ntn))
+    l in
+  interp_recursive Command.IsCoFixpoint fixl b