diff options
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 62 |
1 files changed, 33 insertions, 29 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 1f6e7e83..9b18ef27 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(* $Id: command.ml 13344 2010-07-28 15:04:36Z msozeau $ *) open Pp open Util @@ -69,8 +69,7 @@ let red_constant_entry n ce = function let interp_definition boxed bl red_option c ctypopt = let env = Global.env() in let evdref = ref Evd.empty in - let (env_bl, ctx), imps1 = - interp_context_evars ~fail_anonymous:false evdref env bl in + let (env_bl, ctx), imps1 = interp_context_evars evdref env bl in let imps,ce = match ctypopt with None -> @@ -227,7 +226,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = let env0 = Global.env() in let evdref = ref Evd.empty in let (env_params, ctx_params), userimpls = - interp_context_evars ~fail_anonymous:false evdref env0 paramsl + interp_context_evars evdref env0 paramsl in let indnames = List.map (fun ind -> ind.ind_name) indl in @@ -244,7 +243,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun (_, impls) -> userimpls @ lift_implicits (List.length userimpls) impls) arities in let arities = List.map fst arities in - let impls = compute_full_internalization_env env0 Inductive params indnames fullarities indimpls in + let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -256,9 +255,9 @@ let interp_mutual_inductive (paramsl,indl) notations finite = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_params !evdref in + let evd = consider_remaining_unif_problems env_params !evdref in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in - let sigma = evd in + let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in let arities = List.map (nf_evar sigma) arities in @@ -448,14 +447,19 @@ let check_mutuality env isfix fixl = type structured_fixpoint_expr = { fix_name : identifier; + fix_annot : identifier located option; fix_binders : local_binder list; fix_body : constr_expr option; fix_type : constr_expr } -let interp_fix_context evdref env fix = - interp_context_evars evdref env fix.fix_binders - +let interp_fix_context evdref env isfix fix = + let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in + let (env', ctx), imps = interp_context_evars evdref env before in + let (env'', ctx'), imps' = interp_context_evars evdref env' after in + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + ((env'', ctx' @ ctx), imps @ imps', annot) + let interp_fix_ccl evdref (env,_) fix = interp_type_evars evdref env fix.fix_type @@ -487,8 +491,8 @@ let prepare_recursive_declaration fixnames fixtypes fixdefs = (* Jump over let-bindings. *) -let compute_possible_guardness_evidences na fix (ids,_) = - match index_of_annot fix.fix_binders na with +let compute_possible_guardness_evidences (ids,_,na) = + match na with | Some i -> [i] | None -> (* If recursive argument was not given by user, we try all args. @@ -507,15 +511,15 @@ let interp_recursive isfix fixl notations = (* 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 fixctxs, fiximps, fixannots = + list_split3 (List.map (interp_fix_context evdref env isfix) fixl) in let fixccls = List.map2 (interp_fix_ccl evdref) fixctxs fixl in let fixtypes = List.map2 build_fix_type fixctxs fixccls in let fixtypes = List.map (nf_evar !evdref) fixtypes in let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_full_internalization_env env Recursive [] fixnames fixtypes fiximps in + let impls = compute_internalization_env env Recursive fixnames fixtypes fiximps in (* Interp bodies with rollback because temp use of notations/implicit *) let fixdefs = @@ -525,7 +529,7 @@ let interp_recursive isfix fixl notations = () in (* Instantiate evars and check all are resolved *) - let evd,_ = consider_remaining_unif_problems env_rec !evdref in + let evd = consider_remaining_unif_problems env_rec !evdref in let fixdefs = List.map (Option.map (nf_evar evd)) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let fixctxnames = List.map (fun (_,ctx) -> List.map pi1 ctx) fixctxs in @@ -538,7 +542,7 @@ let interp_recursive isfix fixl notations = end; (* Build the fix declaration block *) - (fixnames,fixdefs,fixtypes),List.combine fixctxnames fiximps + (fixnames,fixdefs,fixtypes), list_combine3 fixctxnames fiximps fixannots let interp_fixpoint = interp_recursive true let interp_cofixpoint = interp_recursive false @@ -547,7 +551,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = - list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -558,7 +562,7 @@ let declare_fixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) indexes ntns = let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let indexes = search_guard dummy_loc (Global.env()) indexes fixdecls in - let fiximps = List.map snd fiximps in + let fiximps = List.map (fun (n,r,p) -> r) fiximps in let fixdecls = list_map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in ignore (list_map4 (declare_fix boxed Fixpoint) fixnames fixdecls fixtypes fiximps); @@ -572,7 +576,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = if List.mem None fixdefs then (* Some bodies to define by proof *) let thms = - list_map3 (fun id t imps -> (id,(t,imps))) fixnames fixtypes fiximps in + list_map3 (fun id t (len,imps,_) -> (id,(t,(len,imps)))) fixnames fixtypes fiximps in let init_tac = Some (List.map (Option.cata Tacmach.refine_no_check Tacticals.tclIDTAC) fixdefs) in @@ -583,7 +587,7 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = let fixdefs = List.map Option.get fixdefs in let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in let fixdecls = list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in - let fiximps = List.map snd fiximps in + let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in ignore (list_map4 (declare_fix boxed CoFixpoint) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames @@ -592,28 +596,28 @@ let declare_cofixpoint boxed ((fixnames,fixdefs,fixtypes),fiximps) ntns = List.iter Metasyntax.add_notation_interpretation ntns let extract_decreasing_argument = function - | (_,(na,CStructRec),_,_,_) -> na + | (na,CStructRec) -> na | _ -> error "Only structural decreasing is supported for a non-Program Fixpoint" let extract_fixpoint_components l = let fixl, ntnl = List.split l in - let wfl = List.map extract_decreasing_argument fixl in - let fixl = List.map (fun ((_,id),_,bl,typ,def) -> - {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in - fixl, List.flatten ntnl, wfl + let fixl = List.map (fun ((_,id),ann,bl,typ,def) -> + let ann = extract_decreasing_argument ann in + {fix_name = id; fix_annot = ann; fix_binders = bl; fix_body = def; fix_type = typ}) fixl in + fixl, List.flatten ntnl let extract_cofixpoint_components l = let fixl, ntnl = List.split l in List.map (fun ((_,id),bl,typ,def) -> - {fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, + {fix_name = id; fix_annot = None; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl let do_fixpoint l b = - let fixl,ntns,wfl = extract_fixpoint_components l in + let fixl,ntns = extract_fixpoint_components l in let fix = interp_fixpoint fixl ntns in let possible_indexes = - list_map3 compute_possible_guardness_evidences wfl fixl (snd fix) in + List.map compute_possible_guardness_evidences (snd fix) in declare_fixpoint b fix possible_indexes ntns let do_cofixpoint l b = |