diff options
Diffstat (limited to 'pretyping/reductionops.ml')
| -rw-r--r-- | pretyping/reductionops.ml | 213 |
1 files changed, 164 insertions, 49 deletions
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9c9877fd23..98ca329117 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -279,7 +279,9 @@ sig | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t + and 'a t = 'a member list exception IncompatibleFold2 @@ -308,6 +310,8 @@ sig val nth : 'a t -> int -> 'a val best_state : evar_map -> constr * constr t -> Cst_stack.t -> constr * constr t val zip : ?refold:bool -> evar_map -> constr * constr t -> constr + val check_native_args : CPrimitives.t -> 'a t -> bool + val get_next_primitive_args : CPrimitives.args_red -> 'a t -> CPrimitives.args_red * ('a t * 'a * 'a t) option end = struct open EConstr @@ -336,7 +340,9 @@ struct | Case of case_info * 'a * 'a array * Cst_stack.t | Proj of Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t + | Primitive of CPrimitives.t * (Constant.t * EInstance.t) * 'a t * CPrimitives.args_red * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t + and 'a t = 'a member list (* Debugging printer *) @@ -354,6 +360,9 @@ struct | Fix (f,args,cst) -> str "ZFix(" ++ Constr.debug_print_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" + | Primitive (p,c,args,kargs,cst_l) -> + str "ZPrimitive(" ++ str (CPrimitives.to_string p) + ++ pr_comma () ++ pr pr_c args ++ str ")" | Cst (mem,curr,remains,params,cst_l) -> str "ZCst(" ++ pr_cst_member pr_c mem ++ pr_comma () ++ int curr ++ pr_comma () ++ @@ -420,7 +429,7 @@ struct equal_cst_member c1 c2 && equal_rec (List.rev params1) (List.rev params2) && equal_rec s1' s2' - | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false + | ((App _|Case _|Proj _|Fix _|Cst _|Primitive _)::_|[]), _ -> false in equal_rec (List.rev sk1) (List.rev sk2) let compare_shape stk1 stk2 = @@ -435,9 +444,11 @@ struct Int.equal bal 0 && compare_rec 0 s1 s2 | (Fix(_,a1,_)::s1, Fix(_,a2,_)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 + | (Primitive(_,_,a1,_,_)::s1, Primitive(_,_,a2,_,_)::s2) -> + Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 | (Cst (_,_,_,p1,_)::s1, Cst (_,_,_,p2,_)::s2) -> - Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2 - | (_,_) -> false in + Int.equal bal 0 && compare_rec 0 p1 p2 && compare_rec 0 s1 s2 + | ((Case _|Proj _|Fix _|Cst _|Primitive _) :: _ | []) ,_ -> false in compare_rec 0 stk1 stk2 exception IncompatibleFold2 @@ -459,7 +470,7 @@ struct | Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 -> let o' = aux o (List.rev params1) (List.rev params2) in aux o' q1 q2 - | (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) -> + | (((App _|Case _|Proj _|Fix _|Cst _|Primitive _) :: _|[]), _) -> raise IncompatibleFold2 in aux o (List.rev sk1) (List.rev sk2) @@ -473,7 +484,9 @@ struct Fix ((r,(na,Array.map f ty, Array.map f bo)),map f arg,alt) | Cst (cst,curr,remains,params,alt) -> Cst (cst,curr,remains,map f params,alt) - ) x + | Primitive (p,c,args,kargs,cst_l) -> + Primitive(p,c, map f args, kargs, cst_l) + ) x let append_app_list l s = let a = Array.of_list l in @@ -481,7 +494,7 @@ struct let rec args_size = function | App (i,_,j)::s -> j + 1 - i + args_size s - | (Case _|Fix _|Proj _|Cst _)::_ | [] -> 0 + | (Case _|Fix _|Proj _|Cst _|Primitive _)::_ | [] -> 0 let strip_app s = let rec aux out = function @@ -504,7 +517,8 @@ struct in aux n [] s let not_purely_applicative args = - List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true | _ -> false) args + List.exists (function (Fix _ | Case _ | Proj _ | Cst _) -> true + | App _ | Primitive _ -> false) args let will_expose_iota args = List.exists (function (Fix (_,_,l) | Case (_,_,_,l) | @@ -588,9 +602,26 @@ struct | f, (Proj (p,cst_l)::s) when refold -> zip (best_state sigma (mkProj (p,f),s) cst_l) | f, (Proj (p,_)::s) -> zip (mkProj (p,f),s) + | f, (Primitive (p,c,args,kargs,cst_l)::s) -> + zip (mkConstU c, args @ append_app [|f|] s) in zip s + (* Check if there is enough arguments on [stk] w.r.t. arity of [op] *) + let check_native_args op stk = + let nargs = CPrimitives.arity op in + let rargs = args_size stk in + nargs <= rargs + + let get_next_primitive_args kargs stk = + let rec nargs = function + | [] -> 0 + | CPrimitives.Kwhnf :: _ -> 0 + | _ :: s -> 1 + nargs s + in + let n = nargs kargs in + (List.skipn (n+1) kargs, strip_n_app n stk) + end (** The type of (machine) states (= lambda-bar-calculus' cuts) *) @@ -815,6 +846,57 @@ let fix_recarg ((recindices,bodynum),_) stack = with Not_found -> None +open Primred + +module CNativeEntries = +struct + + type elem = EConstr.t + type args = EConstr.t array + type evd = evar_map + + let get = Array.get + + let get_int evd e = + match EConstr.kind evd e with + | Int i -> i + | _ -> raise Primred.NativeDestKO + + let mkInt env i = + mkInt i + + let mkBool env b = + let (ct,cf) = get_bool_constructors env in + mkConstruct (if b then ct else cf) + + let mkCarry env b e = + let int_ty = mkConst @@ get_int_type env in + let (c0,c1) = get_carry_constructors env in + mkApp (mkConstruct (if b then c1 else c0),[|int_ty;e|]) + + let mkIntPair env e1 e2 = + let int_ty = mkConst @@ get_int_type env in + let c = get_pair_constructor env in + mkApp(mkConstruct c, [|int_ty;int_ty;e1;e2|]) + + let mkLt env = + let (_eq, lt, _gt) = get_cmp_constructors env in + mkConstruct lt + + let mkEq env = + let (eq, _lt, _gt) = get_cmp_constructors env in + mkConstruct eq + + let mkGt env = + let (_eq, _lt, gt) = get_cmp_constructors env in + mkConstruct gt + +end + +module CredNative = RedNative(CNativeEntries) + + + (** Generic reduction function with environment Here is where unfolded constant are stored in order to be @@ -881,47 +963,55 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack)))); if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then let u' = EInstance.kind sigma u in - (match constant_opt_value_in env (c, u') with - | None -> fold () - | Some body -> + match constant_value_in env (c, u') with + | body -> + begin let body = EConstr.of_constr body in - if not tactic_mode - then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) - (body, stack) - else (* Looks for ReductionBehaviour *) - match ReductionBehaviour.get (Globnames.ConstRef c) with - | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags - || (nargs > 0 && Stack.args_size stack < nargs)) - then fold () - else (* maybe unfolds *) - if List.mem `ReductionDontExposeCase flags then - let app_sk,sk = Stack.strip_app stack in - let (tm',sk'),cst_l' = - whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) - in - let rec is_case x = match EConstr.kind sigma x with - | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x - | App (hd, _) -> is_case hd - | Case _ -> true - | _ -> false in - if equal_stacks sigma (x, app_sk) (tm', sk') - || Stack.will_expose_iota sk' - || is_case tm' - then fold () - else whrec cst_l' (tm', sk' @ sk) - else match recargs with - |[] -> (* if nargs has been specified *) - (* CAUTION : the constant is NEVER refold - (even when it hides a (co)fix) *) - whrec cst_l (body, stack) - |curr::remains -> match Stack.strip_n_app curr stack with - | None -> fold () - | Some (bef,arg,s') -> - whrec Cst_stack.empty - (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') - ) else fold () + if not tactic_mode + then whrec (if refold then Cst_stack.add_cst (mkConstU const) cst_l else cst_l) + (body, stack) + else (* Looks for ReductionBehaviour *) + match ReductionBehaviour.get (Globnames.ConstRef c) with + | None -> whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, stack) + | Some (recargs, nargs, flags) -> + if (List.mem `ReductionNeverUnfold flags + || (nargs > 0 && Stack.args_size stack < nargs)) + then fold () + else (* maybe unfolds *) + if List.mem `ReductionDontExposeCase flags then + let app_sk,sk = Stack.strip_app stack in + let (tm',sk'),cst_l' = + whrec (Cst_stack.add_cst (mkConstU const) cst_l) (body, app_sk) + in + let rec is_case x = match EConstr.kind sigma x with + | Lambda (_,_, x) | LetIn (_,_,_, x) | Cast (x, _,_) -> is_case x + | App (hd, _) -> is_case hd + | Case _ -> true + | _ -> false in + if equal_stacks sigma (x, app_sk) (tm', sk') + || Stack.will_expose_iota sk' + || is_case tm' + then fold () + else whrec cst_l' (tm', sk' @ sk) + else match recargs with + |[] -> (* if nargs has been specified *) + (* CAUTION : the constant is NEVER refold + (even when it hides a (co)fix) *) + whrec cst_l (body, stack) + |curr::remains -> match Stack.strip_n_app curr stack with + | None -> fold () + | Some (bef,arg,s') -> + whrec Cst_stack.empty + (arg,Stack.Cst(Stack.Cst_const (fst const, u'),curr,remains,bef,cst_l)::s') + end + | exception NotEvaluableConst (IsPrimitive p) when Stack.check_native_args p stack -> + let kargs = CPrimitives.kind p in + let (kargs,o) = Stack.get_next_primitive_args kargs stack in + (* Should not fail thanks to [check_native_args] *) + let (before,a,after) = Option.get o in + whrec Cst_stack.empty (a,Stack.Primitive(p,const,before,kargs,cst_l)::after) + | exception NotEvaluableConst _ -> fold () + else fold () | Proj (p, c) when CClosure.RedFlags.red_projection flags p -> (let npars = Projection.npars p in if not tactic_mode then @@ -1049,6 +1139,30 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = |_ -> fold () else fold () + | Int i -> + begin match Stack.strip_app stack with + | (_, Stack.Primitive(p,kn,rargs,kargs,cst_l')::s) -> + let more_to_reduce = List.exists (fun k -> CPrimitives.Kwhnf = k) kargs in + if more_to_reduce then + let (kargs,o) = Stack.get_next_primitive_args kargs s in + (* Should not fail because Primitive is put on the stack only if fully applied *) + let (before,a,after) = Option.get o in + whrec Cst_stack.empty (a,Stack.Primitive(p,kn,rargs @ Stack.append_app [|x|] before,kargs,cst_l')::after) + else + let n = List.length kargs in + let (args,s) = Stack.strip_app s in + let (args,extra_args) = + try List.chop n args + with List.IndexOutOfRange -> (args,[]) (* FIXME probably useless *) + in + let args = Array.of_list (Option.get (Stack.list_of_app_stack (rargs @ Stack.append_app [|x|] args))) in + begin match CredNative.red_prim env sigma p args with + | Some t -> whrec cst_l' (t,s) + | None -> ((mkApp (mkConstU kn, args), s), cst_l) + end + | _ -> fold () + end + | Rel _ | Var _ | LetIn _ | Proj _ -> fold () | Sort _ | Ind _ | Prod _ -> fold () in @@ -1127,7 +1241,8 @@ let local_whd_state_gen flags sigma = |_ -> s else s - | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ -> s + | Rel _ | Var _ | Sort _ | Prod _ | LetIn _ | Const _ | Ind _ | Proj _ + | Int _ -> s in whrec @@ -1577,7 +1692,7 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s = if isConstruct sigma t_o then whrec Cst_stack.empty (Stack.nth stack_o (Projection.npars p + Projection.arg p), stack'') else s,csts' - |_, ((Stack.App _|Stack.Cst _) :: _|[]) -> s,csts' + |_, ((Stack.App _|Stack.Cst _|Stack.Primitive _) :: _|[]) -> s,csts' in whrec csts s let find_conclusion env sigma = |