From 23d402abfa076a5e4f9b538bc4c314884c02b0e4 Mon Sep 17 00:00:00 2001 From: filliatr Date: Thu, 22 Feb 2001 16:42:48 +0000 Subject: extraction des types et des inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1399 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/Extraction.v | 5 +- contrib/extraction/extraction.ml | 337 +++++++++++++++++++++++++++----------- contrib/extraction/extraction.mli | 2 - contrib/extraction/miniml.mli | 28 +++- contrib/extraction/ocaml.ml | 159 ++++++++++++++++++ contrib/extraction/ocaml.mli | 9 + 6 files changed, 439 insertions(+), 101 deletions(-) create mode 100644 contrib/extraction/ocaml.ml create mode 100644 contrib/extraction/ocaml.mli (limited to 'contrib') diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 74a7455f9..9e0f23c2d 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -1,2 +1,5 @@ -Declare ML Module "extraction.cmo". +Declare ML Module "ocaml.cmo" "extraction.cmo". + +Grammar vernac vernac : ast := + extr_constr [ "Extraction" constrarg($c) "." ] -> [(Extraction $c)]. diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 616648143..aa7fadc67 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -8,6 +8,7 @@ open Term open Declarations open Environ open Reduction +open Inductive open Instantiate open Miniml open Mlimport @@ -26,102 +27,178 @@ type extraction_result = | Emltype of ml_type * signature * identifier list | Emlterm of ml_ast +(*s Utility functions. *) + +let array_foldi f a = + let n = Array.length a in + let rec fold i v = if i = n then v else fold (succ i) (f i a.(i) v) in + fold 0 + let flexible_name = id_of_string "flex" let id_of_name = function | Anonymous -> id_of_string "_" | Name id -> id -(*s Extraction of a type. *) +let params_of_sign = + List.fold_left (fun l v -> match v with Vskip,_ -> l | _,id -> id :: l) [] -let rec extract_type c = - let genv = Global.env() in - let rec extract_rec env sign fl c args = match kind_of_term (whd_beta c) with - | IsProd (n, t, d) -> - assert (args = []); - let id = id_of_name n in (* FIXME: capture problem *) +let signature_of_arity = + let rec sign_of acc env c = match kind_of_term c with + | IsProd (n, t, c') -> let env' = push_rel (n,None,t) env in - (match extract_rec env sign fl t [] with - | Tarity -> - extract_rec env' ((Varity,id) :: sign) fl d [] - | Tmltype (t', _, fl') -> - (match extract_rec env' ((Vskip,id) :: sign) fl' d [] with - | Tarity -> Tarity - | Tmltype (d', sign', fl'') -> - Tmltype (Tarr (t', d'), sign', fl''))) - | IsSort (Prop Null) -> - assert (args = []); - Tmltype (Tprop, [], []) - | IsSort _ -> - assert (args = []); - Tarity - | IsApp (d, args') -> - extract_rec env sign fl d (Array.to_list args' @ args) - | IsRel n -> - (match List.nth sign (pred n) with - | Vskip, id -> Tmltype (Tvar id, sign, id :: fl) - | Varity, id -> Tmltype (Tvar id, sign, fl)) - | IsConst (sp,a) -> - let cty = constant_type genv Evd.empty (sp,a) in - if is_arity genv Evd.empty cty then - (match extract_constant sp with - | Emltype (_, sc, flc) -> - assert (List.length sc = List.length args); - let (mlargs,fl') = - List.fold_left - (fun ((args,fl) as acc) (v,a) -> match v with - | Vskip,_ -> acc - | Varity,_ -> match extract_rec env sign fl a [] with - | Tarity -> assert false - | Tmltype (mla,_,fl') -> (mla :: args, fl') - ) - ([],fl) (List.combine sc args) - in - let flc = List.map (fun i -> Tvar i) flc in - Tmltype (Tapp ((Tglob (ConstRef sp)) :: mlargs @ flc), - sign, fl') - | Emlterm _ -> - assert false) - else - failwith "todo: expanse c, reduce and apply recursively" - | IsMutInd _ -> - failwith "todo" - | IsMutCase _ - | IsFix _ -> - let id = next_ident_away flexible_name fl in - Tmltype (Tvar id, sign, id :: fl) - | IsCast (c, _) -> - extract_rec env sign fl c args - | _ -> + let id = id_of_name n in + sign_of + (((if is_arity env Evd.empty t then Varity else Vskip), id) :: acc) + env' c' + | IsSort _ -> + acc + | _ -> assert false in - extract_rec (Global.env()) [] [] c [] + sign_of [] + +(* [list_of_ml_arrows] applied to the ML type [a->b->...->z->t] + returns the list [[a;b;...:z]]. *) +let rec list_of_ml_arrows = function + | Tarr (a, b) -> a :: list_of_ml_arrows b + | t -> [] + +(*s Tables to keep the extraction of inductive types and constructors. *) + +type inductive_extraction_result = signature * identifier list + +let inductive_extraction_table = + ref (Gmap.empty : (inductive_path, inductive_extraction_result) Gmap.t) + +let add_inductive_extraction i e = + inductive_extraction_table := Gmap.add i e !inductive_extraction_table + +let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table + +type constructor_extraction_result = ml_type list * signature + +let constructor_extraction_table = + ref (Gmap.empty : (constructor_path, constructor_extraction_result) Gmap.t) + +let add_constructor_extraction c e = + constructor_extraction_table := Gmap.add c e !constructor_extraction_table + +let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table + +(*i FIXME +let inductive_declaration_table = + ref (Gmap.empty : (section_path, ml_ind list) Gmap.t) + +let add_inductive_declaration sp d = + inductive_declaration_table := Gmap.add +i*) + +(*s Extraction of a type. *) + +let rec extract_type env c = + let genv = Global.env() in + let rec extract_rec env sign fl c args = + let ty = Typing.type_of env Evd.empty c in + if is_Prop (whd_betadeltaiota env Evd.empty ty) then + Tmltype (Tprop, [], fl) + else + match kind_of_term (whd_betaiota c) with + | IsProd (n, t, d) -> + assert (args = []); + let id = id_of_name n in (* FIXME: capture problem *) + let env' = push_rel (n,None,t) env in + (match extract_rec env sign fl t [] with + | Tarity -> + extract_rec env' ((Varity,id) :: sign) fl d [] + | Tmltype (t', _, fl') -> + (match extract_rec env' ((Vskip,id) :: sign) fl' d [] with + | Tarity -> Tarity + | Tmltype (d', sign', fl'') -> + Tmltype (Tarr (t', d'), sign', fl''))) + | IsLambda (n, t, d) -> + assert (args = []); + let id = id_of_name n in (* FIXME: capture problem *) + let env' = push_rel (n,None,t) env in + (match extract_rec env sign fl t [] with + | Tarity -> + extract_rec env' ((Varity,id) :: sign) fl d [] + | Tmltype (t', _, fl') -> + extract_rec env' ((Vskip,id) :: sign) fl' d []) + | IsSort (Prop Null) -> + assert (args = []); + Tmltype (Tprop, [], []) + | IsSort _ -> + assert (args = []); + Tarity + | IsApp (d, args') -> + extract_rec env sign fl d (Array.to_list args' @ args) + | IsRel n -> + (match List.nth sign (pred n) with + | Vskip, id -> Tmltype (Tvar id, sign, id :: fl) + | Varity, id -> Tmltype (Tvar id, sign, fl)) + | IsConst (sp,a) -> + let cty = constant_type genv Evd.empty (sp,a) in + if is_arity env Evd.empty cty then + (match extract_constant sp with + | Emltype (_, sc, flc) -> + extract_type_app env sign fl (ConstRef sp,sc,flc) args + | Emlterm _ -> assert false) + else + let cvalue = constant_value env (sp,a) in + extract_rec env sign fl (mkApp (cvalue, Array.of_list args)) [] + | IsMutInd (spi,_) -> + let (si,fli) = extract_inductive spi in + extract_type_app env sign fl (IndRef spi,si,fli) args + | IsMutCase _ + | IsFix _ -> + let id = next_ident_away flexible_name fl in + Tmltype (Tvar id, sign, id :: fl) + | IsCast (c, _) -> + extract_rec env sign fl c args + | _ -> + assert false + and extract_type_app env sign fl (r,sc,flc) args = + let nargs = List.length args in + assert (List.length sc >= nargs); + let (mlargs,fl') = + List.fold_right + (fun (v,a) ((args,fl) as acc) -> match v with + | Vskip,_ -> acc + | Varity,_ -> match extract_rec env sign fl a [] with + | Tarity -> assert false + | Tmltype (mla,_,fl') -> (mla :: args, fl')) + (List.combine (list_firstn nargs (List.rev sc)) args) + ([],fl) + in + let flc = List.map (fun i -> Tvar i) flc in + Tmltype (Tapp ((Tglob r) :: mlargs @ flc), sign, fl') + in + extract_rec env [] [] c [] + (*s Extraction of a term. *) and extract_term c = failwith "todo" -(*i - let rec extract_rec env c = match kind_of_term (whd_beta c) with - | _ -> - failwith "todo" - | IsSort _ | IsXtra _ | IsVar _ | IsMeta _ -> - assert false - in - extract_rec (Global.env()) c -i*) + (*i + let rec extract_rec env c = match kind_of_term (whd_beta c) with + | _ -> + failwith "todo" + | IsSort _ | IsXtra _ | IsVar _ | IsMeta _ -> + assert false + in + extract_rec (Global.env()) c + i*) (*s Extraction of a constr. *) and extract_constr_with_type c t = - let redt = whd_betadeltaiota (Global.env()) Evd.empty t in - if isSort redt then begin - if is_Prop redt then - Emltype (Tprop, [], []) - else - match extract_type c with - | Tarity -> error "not an ML type" - | Tmltype (t, sign, fl) -> Emltype (t, sign, fl) + let genv = Global.env () in + if is_arity genv Evd.empty t then begin + match extract_type genv c with + | Tarity -> error "not an ML type" + | Tmltype (t, sign, fl) -> Emltype (t, sign, fl) end else let t = extract_term c in Emlterm t @@ -136,28 +213,102 @@ and extract_constant sp = let typ = cb.const_type in let body = match cb.const_body with Some c -> c | None -> assert false in extract_constr_with_type body typ - + (*s Extraction of an inductive. *) -and extract_inductive sp = - let mib = Global.lookup_mind sp in - failwith "todo" - (* Dtype ... *) +and extract_inductive ((sp,_) as i) = + extract_mib sp; + lookup_inductive_extraction i + +and extract_constructor (((sp,_),_) as c) = + extract_mib sp; + lookup_constructor_extraction c + +and extract_mib sp = + if not (Gmap.mem (sp,0) !inductive_extraction_table) then begin + let mib = Global.lookup_mind sp in + let genv = Global.env () in + (* first pass: we store inductive signatures together with empty flex. *) + Array.iteri + (fun i ib -> add_inductive_extraction (sp,i) + (signature_of_arity genv ib.mind_nf_arity, [])) + mib.mind_packets; + (* second pass: we extract constructors arities and we accumulate + all flexible variables. *) + let fl = + array_foldi + (fun i ib fl -> + let mis = build_mis ((sp,i),[||]) mib in + array_foldi + (fun j _ fl -> + let t = mis_constructor_type (succ j) mis in + match extract_type genv t with + | Tarity -> assert false + | Tmltype (mlt, s, f) -> + let l = list_of_ml_arrows mlt in + add_constructor_extraction ((sp,i),succ j) (l,s); + f @ fl) + ib.mind_nf_lc fl) + mib.mind_packets [] + in + (* third pass: we update the inductive flexible variables. *) + for i = 0 to mib.mind_ntypes - 1 do + let (s,_) = lookup_inductive_extraction (sp,i) in + add_inductive_extraction (sp,i) (s,fl) + done + end (*s Extraction of a global reference i.e. a constant or an inductive. *) -and extract_reference = function - | ConstRef sp -> extract_constant sp - | IndRef (sp,_) -> extract_inductive sp - | VarRef _ | ConstructRef _ -> assert false +and extract_inductive_declaration sp = + extract_mib sp; + let mib = Global.lookup_mind sp in + let one_constructor ind j id = + let (t,_) = lookup_constructor_extraction (ind,succ j) in (id, t) + in + let one_inductive i ip = + let (s,fl) = lookup_inductive_extraction (sp,i) in + (params_of_sign s @ fl, ip.mind_typename, + Array.to_list (Array.mapi (one_constructor (sp,i)) ip.mind_consnames)) + in + Dtype (Array.to_list (Array.mapi one_inductive mib.mind_packets)) (*s ML declaration from a reference. *) -let params_of_sign = - List.fold_left (fun l v -> match v with Vskip,_ -> l | _,id -> id :: l) [] +let extract_declaration = function + | ConstRef sp -> + let id = basename sp in (* FIXME *) + (match extract_constant sp with + | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt) + | Emlterm t -> Dglob (id, t)) + | IndRef (sp,_) -> extract_inductive_declaration sp + | ConstructRef ((sp,_),_) -> extract_inductive_declaration sp + | VarRef _ -> assert false + +(*s Registration of vernac commands for extraction. *) + +module Pp = Ocaml.Make(struct let pp_global = Printer.pr_global end) + +open Vernacinterp + +let _ = + vinterp_add "Extraction" + (function + | [VARG_CONSTR ast] -> + (fun () -> + let c = Astterm.interp_constr Evd.empty (Global.env()) ast in + match kind_of_term c with + (* If it is a global reference, then output the declaration *) + | IsConst (sp,_) -> + mSGNL (Pp.pp_decl (extract_declaration (ConstRef sp))) + | IsMutInd (ind,_) -> + mSGNL (Pp.pp_decl (extract_declaration (IndRef ind))) + | IsMutConstruct (cs,_) -> + mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs))) + (* Otherwise, output the ML type or expression *) + | _ -> + match extract_constr c with + | Emltype (t,_,_) -> mSGNL (Pp.pp_type t) + | Emlterm a -> mSGNL (Pp.pp_ast a)) + | _ -> assert false) -let extract_declaration r = - let id = basename (Global.sp_of_global r) in (* FIXME *) - match extract_reference r with - | Emltype (mlt, s, fl) -> Dabbrev (id, params_of_sign s @ fl, mlt) - | Emlterm t -> Dglob (id, t) diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index b42091289..3e6c9c275 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -19,8 +19,6 @@ type extraction_result = val extract_constr : constr -> extraction_result -val extract_reference : global_reference -> extraction_result - (*s ML declaration corresponding to a Coq reference. *) val extract_declaration : global_reference -> ml_decl diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 8493b308e..3d4c7e8f6 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -1,14 +1,17 @@ (*i $Id$ i*) +open Pp open Names open Term -(* identifiers of type are either parameters or type names. *) +(*s Target language for extraction: a core ML called MiniML. *) + +(*s Identifiers of type are either parameters or type names. *) type ml_typeid = identifier -(* ML type expressions. *) +(*s ML type expressions. *) type ml_type = | Tvar of ml_typeid @@ -17,11 +20,11 @@ type ml_type = | Tglob of global_reference | Tprop -(* ML inductive types. *) +(*s ML inductive types. *) type ml_ind = identifier list * identifier * (identifier * ml_type list) list -(* ML terms. *) +(*s ML terms. *) type ml_ast = | MLrel of int @@ -35,10 +38,25 @@ type ml_ast = | MLcast of ml_ast * ml_type | MLmagic of ml_ast -(* ML declarations. *) +(*s ML declarations. *) type ml_decl = | Dtype of ml_ind list | Dabbrev of identifier * (identifier list) * ml_type | Dglob of identifier * ml_ast +(*s Pretty-printing of MiniML in a given concrete syntax is parameterized + by a function [pp_global] that pretty-prints global references. + The resulting pretty-printer is a module of type [Mlpp] providing + functions to print types, terms and declarations. *) + +module type Mlpp_param = sig + val pp_global : global_reference -> std_ppcmds +end + +module type Mlpp = sig + val pp_type : ml_type -> std_ppcmds + val pp_ast : ml_ast -> std_ppcmds + val pp_decl : ml_decl -> std_ppcmds +end + diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml new file mode 100644 index 000000000..b3e2557ae --- /dev/null +++ b/contrib/extraction/ocaml.ml @@ -0,0 +1,159 @@ + +(*i $Id$ i*) + +(*s Production of Ocaml syntax. *) + +open Pp +open Util +open Names +open Term +open Miniml + +(*s Some utility functions. *) + +let string s = [< 'sTR s >] + +let open_par = function true -> string "(" | false -> [<>] + +let close_par = function true -> string ")" | false -> [<>] + +let rec collapse_type_app = function + | (Tapp l1) :: l2 -> collapse_type_app (l1@l2) + | l -> l + +let pp_tuple f = function + | [] -> [< >] + | [x] -> f x + | l -> [< 'sTR "("; + prlist_with_sep (fun () -> [< 'sTR ","; 'sPC >]) f l; + 'sTR ")" >] + +let space_if = function true -> [< 'sPC >] | false -> [<>] + +(*s The pretty-printing functor. *) + +module Make = functor(P : Mlpp_param) -> struct + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +let pp_type t = + let rec pp_rec par = function + | Tvar id -> + string ("'" ^ string_of_id id) + | Tapp l -> + (match collapse_type_app l with + | [] -> assert false + | [t] -> pp_rec par t + | t::l -> [< open_par par; pp_tuple (pp_rec false) l; + space_if (l <>[]); pp_rec false t; close_par par >]) + | Tarr (t1,t2) -> + [< open_par par; pp_rec true t1; 'sPC; 'sTR"->"; 'sPC; + pp_rec false t2; close_par par >] + | Tglob r -> + P.pp_global r + | Tprop -> + string "prop" + in + hOV 0 (pp_rec false t) + +(*s Pretty-printing of expressions. [par] indicates whether + parentheses are needed or not. [env] is the list of names for the + de Bruijn variables. [args] is the list of collected arguments + (already pretty-printed). *) + +let rec pp_expr par env args = + let apply st = match args with + | [] -> st + | _ -> hOV 2 [< open_par par; st; 'sPC; + prlist_with_sep (fun () -> [<'sPC>]) (fun s -> s) args; + close_par par >] + in + function + | MLrel n -> + apply (pr_id (List.nth env (pred n))) + | MLapp (f,args') -> + let stl = List.map (pp_expr true env []) args' in + pp_expr par env (stl @ args) f + | MLlam (id,a) -> + failwith "todo" + (*i + let fl,a' = collect_lambda a in + let fl = rename_bvars env fl in + let st = [< abst (List.rev fl) ; pp_rec false (fl@env) [] a' >] in + if args = [] then + [< open_par par; st; close_par par >] + else + apply [< 'sTR "("; st; 'sTR ")" >] + i*) + | MLglob r -> + apply (P.pp_global r) + | MLcons (_,id,[]) -> + pr_id id + | MLcons (_,id,[a]) -> + [< open_par par; pr_id id; 'sPC; pp_expr true env [] a; + pp_expr true env [] a ; close_par par >] + | MLcons (_,id,args') -> + [< open_par par; pr_id id; 'sPC; + pp_tuple (pp_expr true env []) args'; close_par par >] + | MLcase (t, pv) -> + apply + [< if args<>[] then [< 'sTR"(" >] else open_par par; + v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with"; + 'fNL; 'sTR " "; pp_pat env pv >] ; + if args<>[] then [< 'sTR")" >] else close_par par >] + | MLfix (i,b,idl,al) -> + pp_fix par env (i,b,idl,al) args + | MLexn id -> + [< open_par par; 'sTR "failwith"; 'sPC; + 'qS (string_of_id id); close_par par >] + | MLcast (a,t) -> + [< open_par true; pp_expr false env args a; 'sPC; 'sTR ":"; 'sPC; + pp_type t; close_par true >] + | MLmagic a -> + [< open_par true; 'sTR "Obj.magic"; 'sPC; + pp_expr false env args a; close_par true >] + +and pp_pat env pv = failwith "todo" + +and pp_fix par env f args = failwith "todo" + +let pp_ast = pp_expr false [] [] + +(*s Pretty-printing of inductive types declaration. *) + +let pp_parameters l = + [< pp_tuple (fun id -> string ("'" ^ string_of_id id)) l; space_if (l<>[]) >] + +let pp_one_inductive (pl,name,cl) = + let pp_constructor (id,l) = + [< pr_id id; + match l with + | [] -> [< >] + | _ -> [< 'sTR " of " ; + prlist_with_sep + (fun () -> [< 'sPC ; 'sTR "* " >]) pp_type l >] >] + in + [< pp_parameters pl; pr_id name; 'sTR " ="; 'fNL; + v 0 [< 'sTR " " ; + prlist_with_sep (fun () -> [< 'fNL ; 'sTR " | ">]) + (fun c -> hOV 2 (pp_constructor c)) cl >] >] + +let pp_inductive il = + [< 'sTR "type " ; + prlist_with_sep + (fun () -> [< 'fNL ; 'sTR "and " >]) + (fun i -> pp_one_inductive i) + il; + 'fNL >] + +let pp_decl = function + | Dtype i -> + hOV 0 (pp_inductive i) + | Dabbrev (id, l, t) -> + hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; + pr_id id; 'sPC; 'sTR "="; 'sPC; pp_type t >] + | Dglob (id, a) -> + hOV 0 [< 'sTR "let"; 'sPC; pr_id id; 'sPC; 'sTR "="; 'sPC; pp_ast a >] + +end diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli new file mode 100644 index 000000000..be80e419a --- /dev/null +++ b/contrib/extraction/ocaml.mli @@ -0,0 +1,9 @@ + +(*i $Id$ i*) + +(*s Production of Ocaml syntax. *) + +open Miniml + +module Make : functor(P : Mlpp_param) -> Mlpp + -- cgit v1.2.3