diff options
-rw-r--r-- | plugins/extraction/extract_env.ml | 4 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 70 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 7 | ||||
-rw-r--r-- | plugins/extraction/json.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/miniml.mli | 15 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 90 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 5 | ||||
-rw-r--r-- | plugins/extraction/modutil.ml | 23 | ||||
-rw-r--r-- | plugins/extraction/ocaml.ml | 9 | ||||
-rw-r--r-- | plugins/extraction/scheme.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 71 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 6 |
12 files changed, 166 insertions, 138 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 1d7f61456..3d32398ff 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -498,8 +498,8 @@ let print_structure_to_file (fn,si,mo) dry struc = let d = descr () in reset_renaming_tables AllButExternal; let unsafe_needs = { - mldummy = struct_ast_search ((==) MLdummy) struc; - tdummy = struct_type_search Mlutil.isDummy struc; + mldummy = struct_ast_search Mlutil.isMLdummy struc; + tdummy = struct_type_search Mlutil.isTdummy struc; tunknown = struct_type_search ((==) Tunknown) struc; magic = if lang () != Haskell then false diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 1112c3b89..f4d14af62 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -91,7 +91,7 @@ exception NotDefault of kill_reason let check_default env t = match flag_of_type env t with | _,TypeScheme -> raise (NotDefault Ktype) - | Logic,_ -> raise (NotDefault Kother) + | Logic,_ -> raise (NotDefault Kprop) | _ -> () let is_info_scheme env t = match flag_of_type env t with @@ -103,7 +103,7 @@ let is_info_scheme env t = match flag_of_type env t with let rec type_sign env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> - (if is_info_scheme env t then Keep else Kill Kother) + (if is_info_scheme env t then Keep else Kill Kprop) :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] @@ -137,7 +137,7 @@ let rec type_sign_vl env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then Kill Kother::s, vl + if not (is_info_scheme env t) then Kill Kprop::s, vl else Keep::s, (make_typvar n vl) :: vl | _ -> [],[] @@ -154,25 +154,12 @@ let sign_with_implicits r s nb_params = let implicits = implicits_of_global r in let rec add_impl i = function | [] -> [] - | sign::s -> - let sign' = - if sign == Keep && Int.List.mem i implicits - then Kill Kother else sign - in sign' :: add_impl (succ i) s + | Keep::s when Int.Set.mem i implicits -> + Kill (Kimplicit (r,i)) :: add_impl (i+1) s + | sign::s -> sign :: add_impl (i+1) s in add_impl (1+nb_params) s -(* Enriching a exception message *) - -let rec handle_exn r n fn_name = function - | MLexn s -> - (try Scanf.sscanf s "UNBOUND %d%!" - (fun i -> - assert ((0 < i) && (i <= n)); - MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i))) - with Scanf.Scan_failure _ | End_of_file -> MLexn s) - | a -> ast_map (handle_exn r n fn_name) a - (*S Management of type variable contexts. *) (* A De Bruijn variable context (db) is a context for translating Coq [Rel] @@ -285,10 +272,10 @@ let rec extract_type env db j c args = (match expand env mld with | Tdummy d -> Tdummy d | _ -> - let reason = if lvl == TypeScheme then Ktype else Kother in + let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother + | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with | (_,Some t,_) -> extract_type env db j (lift n t) args @@ -458,7 +445,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if p.ip_logical then raise (I Standard); if not (Int.equal (Array.length p.ip_types) 1) then raise (I Standard); let typ = p.ip_types.(0) in - let l = List.filter (fun t -> not (isDummy (expand env t))) typ in + let l = List.filter (fun t -> not (isTdummy (expand env t))) typ in if not (keep_singleton ()) && Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); @@ -479,7 +466,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let mp = MutInd.modpath kn in let rec select_fields l typs = match l,typs with | [],[] -> [] - | _::l, typ::typs when isDummy (expand env typ) -> + | _::l, typ::typs when isTdummy (expand env typ) -> select_fields l typs | Anonymous::l, typ::typs -> None :: (select_fields l typs) @@ -655,7 +642,7 @@ and extract_maybe_term env mle mlt c = try check_default env (type_of env c); extract_term env mle mlt c [] with NotDefault d -> - put_magic (mlt, Tdummy d) MLdummy + put_magic (mlt, Tdummy d) (MLdummy d) (*s Generic way to deal with an application. *) @@ -723,11 +710,11 @@ and extract_cst_app env mle mlt kn u args = else mla with e when Errors.noncritical e -> mla in - (* For strict languages, purely logical signatures with at least - one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left + (* For strict languages, purely logical signatures lead to a dummy lam + (except when [Kill Ktype] everywhere). So a [MLdummy] is left accordingly. *) let optdummy = match sign_kind s_full with - | UnsafeLogicalSig when lang () != Haskell -> [MLdummy] + | UnsafeLogicalSig when lang () != Haskell -> [MLdummy Kprop] | _ -> [] in (* Different situations depending of the number of arguments: *) @@ -826,8 +813,8 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) assert (Int.equal br_size 1); - let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in - let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in + let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in let e = extract_maybe_term env mle mlt br.(0) in snd (case_expunge s e) end @@ -851,8 +838,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) let ids,e = case_expunge s e in - let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in - (List.rev ids, Pusual r, e') + (List.rev ids, Pusual r, e) in if mi.ind_kind == Singleton then begin @@ -960,8 +946,6 @@ let extract_std_constant env kn body typ = let e = extract_term env mle t' c [] in (* Expunging term and type from dummy lambdas. *) let trm = term_expunge s (ids,e) in - let trm = handle_exn (ConstRef kn) n (fun i -> fst (List.nth rels (i-1))) trm - in trm, type_expunge_from_sign env s t (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *) @@ -979,8 +963,8 @@ let extract_axiom env kn typ = let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in - let types = Array.make n (Tdummy Kother) - and terms = Array.make n MLdummy in + let types = Array.make n (Tdummy Kprop) + and terms = Array.make n (MLdummy Kprop) in let kns = Array.to_list vkn in current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) @@ -1022,7 +1006,7 @@ let extract_constant env kn cb = in match flag_of_type env typ with | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype) - | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother) + | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop) | (Info,TypeScheme) -> (match cb.const_body with | Undef _ -> warn_info (); mk_typ_ax () @@ -1047,7 +1031,7 @@ let extract_constant_spec env kn cb = let typ = Typeops.type_of_constant_type env cb.const_type in match flag_of_type env typ with | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) - | (Logic, Default) -> Sval (r, Tdummy Kother) + | (Logic, Default) -> Sval (r, Tdummy Kprop) | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in (match cb.const_body with @@ -1075,8 +1059,8 @@ let extract_constr env c = reset_meta_count (); let typ = type_of env c in match flag_of_type env typ with - | (_,TypeScheme) -> MLdummy, Tdummy Ktype - | (Logic,_) -> MLdummy, Tdummy Kother + | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype + | (Logic,_) -> MLdummy Kprop, Tdummy Kprop | (Info,Default) -> let mlt = extract_type env [] 1 typ [] in extract_term env Mlenv.empty mlt c [], mlt @@ -1090,7 +1074,7 @@ let extract_inductive env kn = | [] -> [] | t::l -> let l' = filter (succ i) l in - if isDummy (expand env t) || Int.List.mem i implicits then l' + if isTdummy (expand env t) || Int.Set.mem i implicits then l' else t::l' in filter (1+ind.ind_nparams) l in @@ -1102,11 +1086,11 @@ let extract_inductive env kn = (*s Is a [ml_decl] logical ? *) let logical_decl = function - | Dterm (_,MLdummy,Tdummy _) -> true + | Dterm (_,MLdummy _,Tdummy _) -> true | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> - (Array.for_all ((==) MLdummy) av) && - (Array.for_all isDummy tv) + (Array.for_all isMLdummy av) && + (Array.for_all isTdummy tv) | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 37b414207..530eb2ff8 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -200,8 +200,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "Prelude.error" ++ spc () ++ qs s) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ pp_bracket_comment (str s)) | MLmagic a -> pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") diff --git a/plugins/extraction/json.ml b/plugins/extraction/json.ml index 125dc86b8..df79c585e 100644 --- a/plugins/extraction/json.ml +++ b/plugins/extraction/json.ml @@ -153,7 +153,7 @@ let rec json_expr env = function ("what", json_str "expr:exception"); ("msg", json_str s) ] - | MLdummy -> json_dict [("what", json_str "expr:dummy")] + | MLdummy _ -> json_dict [("what", json_str "expr:dummy")] | MLmagic a -> json_dict [ ("what", json_str "expr:coerce"); ("value", json_expr env a) diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index b7dee6cb1..681dceaa0 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -16,11 +16,16 @@ open Globnames object expects, and what these arguments will become in the ML object. *) -(* We eliminate from terms: 1) types 2) logical parts. - [Kother] stands both for logical or other reasons - (for instance user-declared implicit arguments w.r.t. extraction). *) +(* We eliminate from terms: + 1) types + 2) logical parts + 3) user-declared implicit arguments of a constant of constructor +*) -type kill_reason = Ktype | Kother +type kill_reason = + | Ktype + | Kprop + | Kimplicit of global_reference * int (* n-th arg of a cst or construct *) type sign = Keep | Kill of kill_reason @@ -118,7 +123,7 @@ and ml_ast = | MLcase of ml_type * ml_ast * ml_branch array | MLfix of int * Id.t array * ml_ast array | MLexn of string - | MLdummy + | MLdummy of kill_reason | MLaxiom | MLmagic of ml_ast diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 6fc1195fb..402370eec 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -299,10 +299,12 @@ let type_to_signature env t = let isKill = function Kill _ -> true | _ -> false -let isDummy = function Tdummy _ -> true | _ -> false +let isTdummy = function Tdummy _ -> true | _ -> false + +let isMLdummy = function MLdummy _ -> true | _ -> false let sign_of_id = function - | Dummy -> Kill Kother + | Dummy -> Kill Kprop | _ -> Keep (* Classification of signatures *) @@ -310,45 +312,44 @@ let sign_of_id = function type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) let rec sign_kind = function | [] -> EmptySig | Keep :: _ -> NonLogicalSig | Kill k :: s -> - match sign_kind s with - | NonLogicalSig -> NonLogicalSig - | UnsafeLogicalSig -> UnsafeLogicalSig - | SafeLogicalSig | EmptySig -> - if k == Kother then UnsafeLogicalSig else SafeLogicalSig + match k, sign_kind s with + | _, NonLogicalSig -> NonLogicalSig + | Ktype, (SafeLogicalSig | EmptySig) -> SafeLogicalSig + | _, _ -> UnsafeLogicalSig (* Removing the final [Keep] in a signature *) let rec sign_no_final_keeps = function | [] -> [] | k :: s -> - let s' = k :: sign_no_final_keeps s in - match s' with [Keep] -> [] | _ -> s' + match k, sign_no_final_keeps s with + | Keep, [] -> [] + | k, l -> k::l (*s Removing [Tdummy] from the top level of a ML type. *) let type_expunge_from_sign env s t = - let rec expunge s t = - if List.is_empty s then t else match t with - | Tmeta {contents = Some t} -> expunge s t - | Tarr (a,b) -> - let t = expunge (List.tl s) b in - if List.hd s == Keep then Tarr (a, t) else t - | Tglob (r,l) -> - (match env r with - | Some mlt -> expunge s (type_subst_list l mlt) - | None -> assert false) - | _ -> assert false + let rec expunge s t = match s, t with + | [], _ -> t + | Keep :: s, Tarr(a,b) -> Tarr (a, expunge s b) + | Kill _ :: s, Tarr(a,b) -> expunge s b + | _, Tmeta {contents = Some t} -> expunge s t + | _, Tglob (r,l) -> + (match env r with + | Some mlt -> expunge s (type_subst_list l mlt) + | None -> assert false) + | _ -> assert false in let t = expunge (sign_no_final_keeps s) t in if lang () != Haskell && sign_kind s == UnsafeLogicalSig then - Tarr (Tdummy Kother, t) + Tarr (Tdummy Kprop, t) else t let type_expunge env t = @@ -385,7 +386,7 @@ let rec eq_ml_ast t1 t2 = match t1, t2 with | MLfix (i1, id1, t1), MLfix (i2, id2, t2) -> Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2 | MLexn e1, MLexn e2 -> String.equal e1 e2 -| MLdummy, MLdummy -> true +| MLdummy k1, MLdummy k2 -> k1 == k2 | MLaxiom, MLaxiom -> true | MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2 | _ -> false @@ -420,7 +421,7 @@ let ast_iter_rel f = | MLapp (a,l) -> iter n a; List.iter (iter n) l | MLcons (_,_,l) | MLtuple l -> List.iter (iter n) l | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () in iter 0 (*s Map over asts. *) @@ -439,7 +440,7 @@ let ast_map f = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l) | MLtuple l -> MLtuple (List.map f l) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -457,7 +458,7 @@ let ast_map_lift f n = function | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l) | MLtuple l -> MLtuple (List.map (f n) l) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom as a -> a (*s Iter over asts. *) @@ -471,7 +472,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,_,l) | MLtuple l -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) @@ -507,7 +508,7 @@ let nb_occur_match = | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l | MLmagic a -> nb k a - | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0 + | MLglob _ | MLexn _ | MLdummy _ | MLaxiom -> 0 in nb 1 (*s Lifting on terms. @@ -559,7 +560,7 @@ let gen_subst v d t = if i' < 1 then a else if i' <= Array.length v then match v.(i'-1) with - | None -> MLexn ("UNBOUND " ^ string_of_int i') + | None -> assert false | Some u -> ast_lift n u else MLrel (i+d) | a -> ast_map_lift subst n a @@ -813,8 +814,8 @@ let census_add, census_max, census_clean = try h := add k i !h with Not_found -> h := (k, Int.Set.singleton i) :: !h in - let maxf k = - let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in + let maxf () = + let len = ref 0 and lst = ref Int.Set.empty and elm = ref MLaxiom in List.iter (fun (e, s) -> let n = Int.Set.cardinal s in @@ -843,7 +844,7 @@ let factor_branches o typ br = if o.opt_case_cst then (try census_add (branch_as_cst br.(i)) i with Impossible -> ()); done; - let br_factor, br_set = census_max MLdummy in + let br_factor, br_set = census_max () in census_clean (); let n = Int.Set.cardinal br_set in if Int.equal n 0 then None @@ -926,7 +927,7 @@ let iota_gen br hd = in iota 0 hd let is_atomic = function - | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy _ -> true | _ -> false let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false @@ -998,7 +999,7 @@ and simpl_app o a = function let a' = List.map (ast_lift k) a in (l, p, simpl o (MLapp (t,a')))) br in simpl o (MLcase (typ,e,br')) - | (MLdummy | MLexn _) as e -> e + | (MLdummy _ | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) @@ -1049,20 +1050,26 @@ let rec select_via_bl l args = match l,args with (*s [kill_some_lams] removes some head lambdas according to the signature [bl]. This list is build on the identifier list model: outermost lambda is on the right. - [Rels] corresponding to removed lambdas are supposed not to occur, and + [Rels] corresponding to removed lambdas are not supposed to occur + (except maybe in the case of Kimplicit), and the other [Rels] are made correct via a [gen_subst]. Output is not directly a [ml_ast], compose with [named_lams] if needed. *) +let is_impl_kill = function Kill (Kimplicit _) -> true | _ -> false + let kill_some_lams bl (ids,c) = let n = List.length bl in let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in if Int.equal n n' then ids,c - else if Int.equal n' 0 then [],ast_lift (-n) c + else if Int.equal n' 0 && not (List.exists is_impl_kill bl) + then [],ast_lift (-n) c else begin let v = Array.make n None in let rec parse_ids i j = function | [] -> () | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l + | Kill (Kimplicit _ as k) :: l -> + v.(i) <- Some (MLdummy k); parse_ids (i+1) j l | Kill _ :: l -> parse_ids (i+1) j l in parse_ids 0 1 bl; select_via_bl bl ids, gen_subst v (n'-n) c @@ -1100,12 +1107,12 @@ let eta_expansion_sign s (ids,c) = let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels in ids, MLapp (ast_lift (i-1) c, a) | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l + | Kill k :: l -> abs (Dummy :: ids) (MLdummy k :: rels) (i+1) l in abs ids [] 1 s (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas - corresponding to [Del] in [s]. *) + corresponding to [Kill _] in [s]. *) let case_expunge s e = let m = List.length s in @@ -1123,8 +1130,9 @@ let term_expunge s (ids,c) = if List.is_empty s then c else let ids,c = kill_some_lams (List.rev s) (ids,c) in - if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then - MLlam (Dummy, ast_lift 1 c) + if List.is_empty ids && lang () != Haskell && + sign_kind s == UnsafeLogicalSig + then MLlam (Dummy, ast_lift 1 c) else named_lams ids c (*s [kill_dummy_args ids r t] looks for occurrences of [MLrel r] in [t] and @@ -1267,7 +1275,7 @@ let rec ml_size = function | MLfix(_,_,f) -> ml_size_array f | MLletin (_,_,t) -> ml_size t | MLmagic t -> ml_size t - | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0 + | MLglob _ | MLrel _ | MLexn _ | MLdummy _ | MLaxiom -> 0 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 0a71d2c83..c380dfb3e 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -67,7 +67,8 @@ val type_expunge : abbrev_map -> ml_type -> ml_type val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type val eq_ml_type : ml_type -> ml_type -> bool -val isDummy : ml_type -> bool +val isTdummy : ml_type -> bool +val isMLdummy : ml_ast -> bool val isKill : sign -> bool val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast @@ -125,8 +126,8 @@ exception Impossible type sign_kind = | EmptySig | NonLogicalSig (* at least a [Keep] *) - | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *) | SafeLogicalSig (* only [Kill Ktype] *) + | UnsafeLogicalSig (* No [Keep], not all [Kill Ktype] *) val sign_kind : signature -> sign_kind diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 53c9f5987..e8383bda5 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -100,7 +100,7 @@ let ast_iter_references do_term do_cons do_type a = Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _ - | MLdummy | MLaxiom | MLmagic _ -> () + | MLdummy _ | MLaxiom | MLmagic _ -> () in iter a let ind_iter_references do_term do_cons do_type kn ind = @@ -387,16 +387,15 @@ let is_prefix pre s = in is_prefix_aux 0 -let check_implicits = function - | MLexn s -> - if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then - begin - if is_prefix "UNBOUND" s then assert false; - if is_prefix "IMPLICIT" s then - error_non_implicit (String.sub s 9 (String.length s - 9)); - end; - false - | _ -> false +exception RemainingImplicit of kill_reason + +let check_for_remaining_implicits struc = + let check = function + | MLdummy (Kimplicit _ as k) -> raise (RemainingImplicit k) + | _ -> false + in + try ignore (struct_ast_search check struc) + with RemainingImplicit k -> err_or_warn_remaining_implicit k let optimize_struct to_appear struc = let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in @@ -415,5 +414,5 @@ let optimize_struct to_appear struc = depcheck_struct opt_struc end in - ignore (struct_ast_search check_implicits mini_struc); + let () = check_for_remaining_implicits mini_struc in mini_struc diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 45f5614af..257c6e971 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -199,8 +199,11 @@ let rec pp_expr par env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)")) - | MLdummy -> - str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy k -> + (* An [MLdummy] may be applied, but I don't really care. *) + (match msg_of_implicit k with + | "" -> str "__" + | s -> str "__" ++ spc () ++ str ("(* "^s^" *)")) | MLmagic a -> pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) | MLaxiom -> @@ -352,7 +355,7 @@ and pp_function env t = | MLcase(Tglob(r,_),MLrel 1,pv) when not (is_coinductive r) && List.is_empty (get_record_fields r) && not (is_custom_match pv) -> - if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then + if not (ast_occurs 1 (MLcase(Tunknown,MLaxiom,pv))) then pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ v 0 (pp_pat env' pv) diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml index cc8b6d8e7..4901cf180 100644 --- a/plugins/extraction/scheme.ml +++ b/plugins/extraction/scheme.ml @@ -126,7 +126,7 @@ let rec pp_expr env args = | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) paren (str "error" ++ spc () ++ qs s) - | MLdummy -> + | MLdummy _ -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLmagic a -> pp_expr env args a diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a57c39eef..63d792e36 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -401,16 +401,34 @@ let error_MPfile_as_mod mp b = "Monolithic Extraction cannot deal with this situation.\n"^ "Please "^s2^"use (Recursive) Extraction Library instead.\n")) -let msg_non_implicit r n id = - let name = match id with - | Anonymous -> "" - | Name id -> "(" ^ Id.to_string id ^ ") " - in - "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r) - -let error_non_implicit msg = - err (str (msg ^ " still occurs after extraction.") ++ - fnl () ++ str "Please check the Extraction Implicit declarations.") +let argnames_of_global r = + let typ = Global.type_of_global_unsafe r in + let rels,_ = + decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in + List.rev_map fst rels + +let msg_of_implicit = function + | Kimplicit (r,i) -> + let name = match List.nth (argnames_of_global r) (i-1) with + | Anonymous -> "" + | Name id -> "(" ^ Id.to_string id ^ ") " + in + (String.ordinal i)^" argument "^name^"of "^(string_of_global r) + | Ktype | Kprop -> "" + +let error_remaining_implicit k = + let s = msg_of_implicit k in + err (str ("An implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Please check your Extraction Implicit declarations." ++ fnl() ++ + str "You might also try Unset Extraction SafeImplicits to force" ++ + fnl() ++ str "the extraction of unsafe code and review it manually.") + +let warning_remaining_implicit k = + let s = msg_of_implicit k in + msg_warning + (str ("At least an implicit occurs after extraction : "^s^".") ++ fnl () ++ + str "Extraction SafeImplicits is unset, extracting nonetheless," ++ fnl () + ++ str "but this code is potentially unsafe, please review it manually.") let check_loaded_modfile mp = match base_mp mp with | MPfile dp -> @@ -635,32 +653,39 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) (*s Extraction Implicit *) +let safe_implicit = my_bool_option "SafeImplicits" true + +let err_or_warn_remaining_implicit k = + if safe_implicit () then + error_remaining_implicit k + else + warning_remaining_implicit k + type int_or_id = ArgInt of int | ArgId of Id.t let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit" let implicits_of_global r = - try Refmap'.find r !implicits_table with Not_found -> [] + try Refmap'.find r !implicits_table with Not_found -> Int.Set.empty let add_implicits r l = - let typ = Global.type_of_global_unsafe r in - let rels,_ = - decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in - let names = List.rev_map fst rels in + let names = argnames_of_global r in let n = List.length names in - let check = function + let add_arg s = function | ArgInt i -> - if 1 <= i && i <= n then i + if 1 <= i && i <= n then Int.Set.add i s else err (int i ++ str " is not a valid argument number for " ++ safe_pr_global r) | ArgId id -> - (try List.index Name.equal (Name id) names - with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ - safe_pr_global r)) + try + let i = List.index Name.equal (Name id) names in + Int.Set.add i s + with Not_found -> + err (str "No argument " ++ pr_id id ++ str " for " ++ + safe_pr_global r) in - let l' = List.map check l in - implicits_table := Refmap'.add r l' !implicits_table + let ints = List.fold_left add_arg Int.Set.empty l in + implicits_table := Refmap'.add r ints !implicits_table (* Registration of operations for rollback. *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 648f23211..a6734dae8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -38,8 +38,8 @@ val error_MPfile_as_mod : module_path -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -val msg_non_implicit : global_reference -> int -> Name.t -> string -val error_non_implicit : string -> 'a +val msg_of_implicit : kill_reason -> string +val err_or_warn_remaining_implicit : kill_reason -> unit val info_file : string -> unit @@ -166,7 +166,7 @@ val to_keep : global_reference -> bool (*s Table for implicits arguments *) -val implicits_of_global : global_reference -> int list +val implicits_of_global : global_reference -> Int.Set.t (*s Table for user-given custom ML extractions. *) |