diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-03 14:02:24 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-03 14:02:24 +0000 |
commit | 231d0032cc337aa8116caa16635d10d2aa91fffb (patch) | |
tree | 51f075e58d325d9fa70811b3227c7f542d4b0188 /contrib/extraction | |
parent | d4a0c133b0b5abb0520969a74f1e2b3819c8435b (diff) |
commandes Extract Constant/Inductive; message d'erreur pour les axiomes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1526 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/Extraction.v | 21 | ||||
-rw-r--r-- | contrib/extraction/TODO | 5 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 187 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 12 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 93 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 19 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 27 |
7 files changed, 238 insertions, 126 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 1f71ef2f2..a5e7c81af 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -16,5 +16,24 @@ Grammar vernac vernac : ast := | extr_list [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] -> [ (ExtractionFile $f ($LIST $l)) ] | extr_module [ "Extraction" "Module" identarg($m) "." ] -> - [ (ExtractionModule $m) ]. + [ (ExtractionModule $m) ] +| extract_constant + [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] + -> [ (EXTRACT_CONSTANT $x $y) ] + +| extract_inductive + [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."] + -> [ (EXTRACT_INDUCTIVE $x $y) ] + +with mindnames : ast := + mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ] + -> [(VERNACARGLIST $id ($LIST $idl))] + +with idorstring_list: List := + ids_nil [ ] -> [ ] +| ids_cons [ idorstring($x) idorstring_list($l) ] -> [ $x ($LIST $l) ] + +with idorstring : ast := + ids_ident [ identarg($id) ] -> [ $id ] +| ids_string [ stringarg($s) ] -> [ $s ]. diff --git a/contrib/extraction/TODO b/contrib/extraction/TODO index 3bef00804..58f655b48 100644 --- a/contrib/extraction/TODO +++ b/contrib/extraction/TODO @@ -3,3 +3,8 @@ 3. Axiomes + 4. Cofix : seulement en Haskell + + 5. Syntaxe Haskell + + 6. Reset sur les commandes Extract Constant/Inductive diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 45f76a311..7eddb932c 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -1,130 +1,90 @@ open Pp +open Util open Term open Lib open Extraction open Miniml open Mlutil -(*s Topological sort of global CIC references. - We introduce graphs of global references; a graph is a map - from edges to the set of their immediate successors. *) - -module Refmap = - Map.Make(struct type t = global_reference let compare = compare end) - -module Refset = - Set.Make(struct type t = global_reference let compare = compare end) - -type graph = Refset.t Refmap.t - -let empty = Refmap.empty - -let add_arc x y g = - let s = try Refmap.find x g with Not_found -> Refset.empty in - let g' = Refmap.add x (Refset.add y s) g in - if not (Refmap.mem y g') then Refmap.add y Refset.empty g' else g' - -exception Found of global_reference - -let maximum g = - try - Refmap.iter (fun x s -> if s = Refset.empty then raise (Found x)) g; - assert false - with Found m -> - m - -let remove m g = - let g' = - Refmap.fold (fun x s -> Refmap.add x (Refset.remove m s)) g Refmap.empty - in - Refmap.remove m g' - -let sorted g = - let rec sorted_aux acc g = - if g = Refmap.empty then - acc - else - let max = maximum g in - sorted_aux (max :: acc) (remove max g) +(*s Recursive computation of the global references to extract. + We use a set of functions visiting the extracted objects in + a depth-first way ([visit_type], [visit_ast] and [visit_decl]). + We maintain an (imperative) structure [extracted_env] containing + the set of already visited references and the list of + references to extract. The entry point is the function [visit_reference]: + it first normalizes the reference, and then check it has already been + visisted; if not, it adds it to the set of visited references, then + recursively traverses its extraction and finally adds it to the + list of references to extract. *) + +type extracted_env = { + mutable visited : Refset.t; + mutable to_extract : global_reference list +} + +let empty () = { visited = ml_extractions (); to_extract = [] } + +let rec visit_reference eenv r = + let r' = match r with + | ConstructRef ((sp,_),_) -> IndRef (sp,0) + | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0) + | _ -> r in - sorted_aux [] g - -(*s Computation of the global references appearing in an AST of a - declaration. *) - -let globals_of_type t = - let rec collect s = function - | Tglob r -> Refset.add r s - | Tapp l -> List.fold_left collect s l - | Tarr (t1,t2) -> collect (collect s t1) t2 - | Tvar _ | Tprop | Tarity -> s + if not (Refset.mem r' eenv.visited) then begin + (* we put [r'] in [visited] first to avoid loops in inductive defs *) + eenv.visited <- Refset.add r' eenv.visited; + visit_decl eenv (extract_declaration r); + eenv.to_extract <- r' :: eenv.to_extract + end + +and visit_type eenv t = + let rec visit = function + | Tglob r -> visit_reference eenv r + | Tapp l -> List.iter visit l + | Tarr (t1,t2) -> visit t1; visit t2 + | Tvar _ | Tprop | Tarity -> () in - collect Refset.empty t - -let globals_of_ast a = - let rec collect s = function - | MLglob r -> Refset.add r s - | MLapp (a,l) -> List.fold_left collect (collect s a) l - | MLlam (_,a) -> collect s a - | MLletin (_,a,b) -> collect (collect s a) b - | MLcons (r,_,l) -> List.fold_left collect (Refset.add r s) l + visit t + +and visit_ast eenv a = + let rec visit = function + | MLglob r -> visit_reference eenv r + | MLapp (a,l) -> visit a; List.iter visit l + | MLlam (_,a) -> visit a + | MLletin (_,a,b) -> visit a; visit b + | MLcons (r,_,l) -> visit_reference eenv r; List.iter visit l | MLcase (a,br) -> - Array.fold_left - (fun s (r,_,a) -> collect (Refset.add r s) a) (collect s a) br - | MLfix (_,_,l) -> List.fold_left collect s l - | MLcast (a,t) -> Refset.union (collect s a) (globals_of_type t) - | MLmagic a -> collect s a - | MLrel _ | MLprop | MLarity | MLexn _ -> s + visit a; Array.iter (fun (r,_,a) -> visit_reference eenv r; visit a) br + | MLfix (_,_,l) -> List.iter visit l + | MLcast (a,t) -> visit a; visit_type eenv t + | MLmagic a -> visit a + | MLrel _ | MLprop | MLarity | MLexn _ -> () in - collect Refset.empty a + visit a -let globals_of_inductive inds = - let globals_of_constructor ie (r,tl) = - List.fold_left - (fun (i,e) t -> Refset.add r i, Refset.union (globals_of_type t) e) ie tl - in - let globals_of_ind (i,e) (_,r,cl) = - List.fold_left globals_of_constructor (Refset.add r i, e) cl - in - let (i,e) = List.fold_left globals_of_ind (Refset.empty,Refset.empty) inds in - Refset.diff e i +and visit_inductive eenv inds = + let visit_constructor (_,tl) = List.iter (visit_type eenv) tl in + let visit_ind (_,_,cl) = List.iter visit_constructor cl in + List.iter visit_ind inds -let globals_of_decl = function +and visit_decl eenv = function | Dtype inds -> - globals_of_inductive inds - | Dabbrev (r,_,t) -> - Refset.remove r (globals_of_type t) - | Dglob (r,a) -> - Refset.remove r (globals_of_ast a) - -(*s Recursive extraction of a piece of environment. *) + visit_inductive eenv inds + | Dabbrev (_,_,t) -> + visit_type eenv t + | Dglob (_,a) -> + visit_ast eenv a -let add_dependency r r' g = - let normalize = function - | ConstructRef ((sp,_),_) -> IndRef (sp,0) - | IndRef (sp,i) as r -> if i = 0 then r else IndRef (sp,0) - | r -> r - in - add_arc (normalize r') (normalize r) g +(*s Recursive extracted environment for a list of reference: we just + iterate [visit_reference] on the list, starting with an empty + extracted environment, and we return the reversed list of + references in the field [to_extract]. *) let extract_env rl = - let rec extract graph seen todo = - if Refset.equal todo Refset.empty then - sorted graph - else - let r = Refset.choose todo in - let todo' = Refset.remove r todo in - if Refset.mem r seen then - extract graph seen todo' - else - let d = extract_declaration r in - let deps = globals_of_decl d in - let graph' = Refset.fold (add_dependency r) deps graph in - extract graph' (Refset.add r seen) (Refset.union todo' deps) - in - extract empty Refset.empty (List.fold_right Refset.add rl Refset.empty) - + let eenv = empty () in + List.iter (visit_reference eenv) rl; + List.rev eenv.to_extract (*s Registration of vernac commands for extraction. *) @@ -139,7 +99,7 @@ module Pp = Ocaml.Make(ToplevelParams) open Vernacinterp let _ = - overwriting_vinterp_add "Extraction" + vinterp_add "Extraction" (function | [VARG_CONSTR ast] -> (fun () -> @@ -160,8 +120,13 @@ let _ = | Eprop -> message "prop") | _ -> assert false) +let no_such_reference q = + errorlabstrm "reference_of_varg" + [< Nametab.pr_qualid q; 'sTR ": no such reference" >] + let reference_of_varg = function - | VARG_QUALID q -> Nametab.locate q + | VARG_QUALID q -> + (try Nametab.locate q with Not_found -> no_such_reference q) | _ -> assert false let decl_of_vargl vl = diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 85a448057..2788fa811 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -250,6 +250,12 @@ let decompose_lam_eta n env c = let rec abstract_n n a = if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a)) +(*s Error message when extraction ends on an axiom. *) + +let axiom_message sp = + errorlabstrm "axiom_message" + [< 'sTR "You must specify an extraction for axiom"; 'sPC; + pr_sp sp; 'sPC; 'sTR "first" >] (*s Tables to keep the extraction of inductive types and constructors. *) @@ -602,10 +608,12 @@ and extract_constant sp = try Gmap.find sp !constant_table with Not_found -> - (* TODO: Axioms *) let cb = Global.lookup_constant sp in let typ = cb.const_type in - let body = match cb.const_body with Some c -> c | None -> assert false in + let body = match cb.const_body with + | Some c -> c + | None -> axiom_message sp + in let e = extract_constr_with_type (Global.env()) [] body typ in constant_table := Gmap.add sp e !constant_table; e diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 7f5b23901..8bc026dae 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -1,4 +1,8 @@ +open Pp +open Names +open Term +open Declarations open Util open Miniml @@ -177,3 +181,92 @@ let uncurrify_decl = function | Dglob (id, a) -> Dglob (id, uncurrify_ast a) | d -> d +(*s Table for direct ML extractions. *) + +module Refset = + Set.Make(struct type t = global_reference let compare = compare end) + +module Refmap = + Map.Make(struct type t = global_reference let compare = compare end) + +let extractions = ref (Refmap.empty, Refset.empty) + +let ml_extractions () = snd !extractions + +let add_ml_extraction r s = + let (map,set) = !extractions in + extractions := (Refmap.add r s map, Refset.add r set) + +let is_ml_extraction r = Refset.mem r (snd !extractions) + +let find_ml_extraction r = Refmap.find r (fst !extractions) + +(*s Registration for rollback. *) + +open Summary + +let _ = declare_summary "ML extractions" + { freeze_function = (fun () -> !extractions); + unfreeze_function = ((:=) extractions); + init_function = + (fun () -> extractions := (Refmap.empty, Refset.empty)); + survive_section = true } + +(*s Grammar entries. *) + +open Vernacinterp + +let string_of_varg = function + | VARG_IDENTIFIER id -> string_of_id id + | VARG_STRING s -> s + | _ -> assert false + +let no_such_reference q = + errorlabstrm "reference_of_varg" + [< Nametab.pr_qualid q; 'sTR ": no such reference" >] + +let reference_of_varg = function + | VARG_QUALID q -> + (try Nametab.locate q with Not_found -> no_such_reference q) + | _ -> assert false + +(*s \verb!Extract Constant qualid => string! *) + +let extract_constant r s = match r with + | ConstRef _ -> + add_ml_extraction r s + | _ -> + errorlabstrm "extract_constant" + [< Printer.pr_global r; 'sPC; 'sTR "is not a constant" >] + +let _ = + vinterp_add "EXTRACT_CONSTANT" + (function + | [id; s] -> + (fun () -> + extract_constant (reference_of_varg id) (string_of_varg s)) + | _ -> assert false) + +(*s \verb!Extract Inductive qualid => string [ string ... string ]! *) + +let extract_inductive r (id2,l2) = match r with + | IndRef ((sp,i) as ip) -> + add_ml_extraction r id2; + let mib = Global.lookup_mind sp in + let n = Array.length mib.mind_packets.(i).mind_consnames in + if n <> List.length l2 then + error "not the right number of constructors"; + list_iter_i + (fun j s -> add_ml_extraction (ConstructRef (ip,succ j)) s) l2 + | _ -> + errorlabstrm "extract_inductive" + [< Printer.pr_global r; 'sPC; 'sTR "is not an inductive type" >] + +let _ = + vinterp_add "EXTRACT_INDUCTIVE" + (function + | [q1; VARG_VARGLIST (id2 :: l2)] -> + (fun () -> + extract_inductive (reference_of_varg q1) + (string_of_varg id2, List.map string_of_varg l2)) + | _ -> assert false) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index b60a3fdf9..7b7a20dd2 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -1,8 +1,15 @@ +open Names +open Term open Miniml -val anonymous : Names.identifier -val prop_name : Names.identifier +(*s Special identifiers. [prop_name] is to be used for propositions + and will be printed as [_] in concrete (Caml) code. *) + +val anonymous : identifier +val prop_name : identifier + +(*s Utility functions over ML terms. *) val occurs : int -> ml_ast -> bool @@ -16,3 +23,11 @@ val betared_decl : ml_decl -> ml_decl val uncurrify_ast : ml_ast -> ml_ast val uncurrify_decl : ml_decl -> ml_decl + +(*s Table for the extraction to ML values. *) + +module Refset : Set.S with type elt = global_reference + +val find_ml_extraction : global_reference -> string + +val ml_extractions : unit -> Refset.t diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 1037772e2..6c073d42e 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -125,6 +125,13 @@ let pr_binding = function module Make = functor(P : Mlpp_param) -> struct +let pp_reference f r = + try let s = find_ml_extraction r in [< 'sTR s >] + with Not_found -> f r + +let pp_type_global = pp_reference P.pp_type_global +let pp_global = pp_reference P.pp_global + (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -143,7 +150,7 @@ let rec pp_type par t = [< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; pp_rec false t2; close_par par >] | Tglob r -> - P.pp_type_global r + pp_type_global r | Tprop -> string "prop" | Tarity -> @@ -184,14 +191,14 @@ let rec pp_expr par env args = 'sPC; pp_expr false env' [] a2 >] | MLglob r -> - apply (P.pp_global r) + apply (pp_global r) | MLcons (r,_,[]) -> - P.pp_global r + pp_global r | MLcons (r,_,[a]) -> - [< open_par par; P.pp_global r; 'sPC; + [< open_par par; pp_global r; 'sPC; pp_expr true env [] a; close_par par >] | MLcons (r,_,args') -> - [< open_par par; P.pp_global r; 'sPC; + [< open_par par; pp_global r; 'sPC; pp_tuple (pp_expr true env []) args'; close_par par >] | MLcase (t, pv) -> apply @@ -224,7 +231,7 @@ and pp_pat env pv = | MLcase _ -> true | _ -> false in - hOV 2 [< P.pp_global name; + hOV 2 [< pp_global name; begin match ids with | [] -> [< >] | _ -> [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >] @@ -292,7 +299,7 @@ let pp_parameters l = let pp_one_inductive (pl,name,cl) = let pp_constructor (id,l) = - [< P.pp_global id; + [< pp_global id; match l with | [] -> [< >] | _ -> [< 'sTR " of " ; @@ -300,7 +307,7 @@ let pp_one_inductive (pl,name,cl) = (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >] >] in - [< pp_parameters pl; P.pp_global name; 'sTR " ="; + [< pp_parameters pl; pp_global name; 'sTR " ="; if cl = [] then [< 'sTR " unit (* empty inductive *)" >] else @@ -326,7 +333,7 @@ let pp_decl = function hOV 0 (pp_inductive i) | Dabbrev (r, l, t) -> hOV 0 [< 'sTR "type"; 'sPC; pp_parameters l; - P.pp_type_global r; 'sPC; 'sTR "="; 'sPC; + pp_type_global r; 'sPC; 'sTR "="; 'sPC; pp_type false t; 'fNL >] | Dglob (r, MLfix (_,[_],[def])) -> let id = P.rename_global r in @@ -334,7 +341,7 @@ let pp_decl = function [< hOV 2 (pp_fix false env' None ([id],[def]) []) >] | Dglob (r, a) -> hOV 0 [< 'sTR "let "; - pp_function (empty_env ()) (P.pp_global r) a; 'fNL >] + pp_function (empty_env ()) (pp_global r) a; 'fNL >] let pp_type = pp_type false let pp_ast a = pp_ast (betared_ast (uncurrify_ast a)) |