aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/extraction/extract_env.ml4
-rw-r--r--plugins/extraction/extraction.ml70
-rw-r--r--plugins/extraction/haskell.ml7
-rw-r--r--plugins/extraction/json.ml2
-rw-r--r--plugins/extraction/miniml.mli15
-rw-r--r--plugins/extraction/mlutil.ml90
-rw-r--r--plugins/extraction/mlutil.mli5
-rw-r--r--plugins/extraction/modutil.ml23
-rw-r--r--plugins/extraction/ocaml.ml9
-rw-r--r--plugins/extraction/scheme.ml2
-rw-r--r--plugins/extraction/table.ml71
-rw-r--r--plugins/extraction/table.mli6
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. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 07:42:36 +0000