diff options
Diffstat (limited to 'contrib/subtac/subtac_command.ml')
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 466 |
1 files changed, 0 insertions, 466 deletions
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml deleted file mode 100644 index c8c7ff72..00000000 --- a/contrib/subtac/subtac_command.ml +++ /dev/null @@ -1,466 +0,0 @@ -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 (Evd.evars_of !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 (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.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 (Evd.evars_of !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 (Evd.evars_of !isevars) Evd.empty fullctyp in - let evm = evars_of_term (Evd.evars_of !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 = evars_of 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.create_evar_defs 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_state_protection (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 (evars_of evd)) fixdefs in - let fixtypes = List.map (nf_evar (evars_of evd)) fixtypes in - let rec_sign = nf_named_context_evar (evars_of 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 = Evd.evars_of 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 |