--- /dev/null
+PACKAGE = ng_extraction
+PREDICATES =
+
+INTERFACE_FILES = \
+ nCicExtraction.mli \
+ coq.mli \
+ ocamlExtractionTable.mli \
+ mlutil.mli \
+ common.mli \
+ extraction.mli \
+ ocaml.mli \
+ ocamlExtraction.mli
+# extract_env.mli \
+
+IMPLEMENTATION_FILES = \
+ miniml.ml $(INTERFACE_FILES:%.mli=%.ml)
+EXTRA_OBJECTS_TO_INSTALL =
+EXTRA_OBJECTS_TO_CLEAN =
+%.cmo: OCAMLOPTIONS += -w Ae
+%.cmi: OCAMLOPTIONS += -w Ae
+%.cmx: OCAMLOPTIONS += -w Ae
+
+include ../../Makefile.defs
+include ../Makefile.common
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+open Coq
+open OcamlExtractionTable
+open Miniml
+open Mlutil
+
+(*s Some pretty-print utility functions. *)
+
+let pp_par par st = if par then str "(" ++ st ++ str ")" else st
+
+let pp_apply st par args = match args with
+ | [] -> st
+ | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
+
+let pr_binding = function
+ | [] -> mt ()
+ | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+
+(** By default, in module Format, you can do horizontal placing of blocks
+ even if they include newlines, as long as the number of chars in the
+ blocks are less that a line length. To avoid this awkward situation,
+ we attach a big virtual size to [fnl] newlines. *)
+
+let fnl () = stras (1000000,"") ++ fnl ()
+
+let fnl2 () = fnl () ++ fnl ()
+
+let space_if = function true -> str " " | false -> mt ()
+
+let is_invalid_id s =
+ match s.[0] with 'a' .. 'z' | 'A' .. 'Z' -> false | _ -> true
+
+let rec lowercase_id id =
+ if id = "" then "x" else
+ if id.[0] = '_' then lowercase_id (String.sub id 1 (String.length id - 1)) else
+ if is_invalid_id id then lowercase_id ("x" ^ id) else
+ String.uncapitalize id
+
+let rec uppercase_id id =
+ if id = "" then "T" else
+ if id.[0] = '_' then uppercase_id (String.sub id 1 (String.length id - 1)) else
+ if is_invalid_id id then uppercase_id ("x" ^ id) else
+ String.capitalize id
+
+type kind = Term | Type | Cons
+
+let upperkind = function
+ | Type
+ | Term -> false
+ | Cons -> true
+
+let kindcase_id k id =
+ if upperkind k then uppercase_id id else lowercase_id id
+
+(*s de Bruijn environments for programs *)
+
+type env = identifier list * Idset.t
+
+(*s Generic renaming issues for local variable names. *)
+
+let rec rename_id id avoid =
+ if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+
+let rec rename_vars avoid = function
+ | [] ->
+ [], avoid
+ | id :: idl when id == dummy_name ->
+ (* we don't rename dummy binders *)
+ let (idl', avoid') = rename_vars avoid idl in
+ (id :: idl', avoid')
+ | id :: idl ->
+ let (idl, avoid) = rename_vars avoid idl in
+ let id = rename_id (lowercase_id id) avoid in
+ (id :: idl, Idset.add id avoid)
+
+let rename_tvars avoid l =
+ let rec rename avoid = function
+ | [] -> [],avoid
+ | id :: idl ->
+ let id = rename_id (lowercase_id id) avoid in
+ let idl, avoid = rename (Idset.add id avoid) idl in
+ (id :: idl, avoid) in
+ fst (rename avoid l)
+
+let push_vars ids (db,avoid) =
+ let ids',avoid' = rename_vars avoid ids in
+ ids', (ids' @ db, avoid')
+
+let get_db_name n (db,_) =
+ let id = List.nth db (pred n) in
+ if id = dummy_name then "__" else id
+
+let empty_env status = [], get_global_ids status
+
+let fake_spec = NReference.Fix (0,-1,-1)
+
+let safe_name_of_reference status r =
+ match r with
+ NReference.Ref (uri, spec) when spec = fake_spec ->
+ (* The field of a record *)
+ NUri.name_of_uri uri
+ | _ -> NCicPp.r2s status true r
+
+let maybe_capitalize b n = if b then String.capitalize n else n
+
+let modname_of_filename status capitalize name =
+ try
+ let name = modname_of_filename status name in
+ status, maybe_capitalize capitalize name
+ with Not_found ->
+ let globs = Idset.elements (get_modnames status) in
+ let s = next_ident_away (String.uncapitalize name) globs in
+ let status = add_modname status s in
+ let status = add_modname_for_filename status name s in
+ status, maybe_capitalize capitalize s
+
+let ref_renaming status (k,r) =
+ let status,s =
+ let rec ref_renaming status (k,r) =
+ try status,name_of_reference status r
+ with Not_found ->
+ if is_projection status r then
+ (* The reference for the projection and the field of a record are different
+ and they would be assigned different names (name clash!). So we normalize
+ the projection reference into the field reference *)
+ let NReference.Ref (uri,_) = r in
+ let fieldref = NReference.reference_of_spec uri fake_spec in
+ ref_renaming status (k,fieldref)
+ else
+ let name = safe_name_of_reference status r in
+ let globs = Idset.elements (get_global_ids status) in
+ let s = next_ident_away (kindcase_id k name) globs in
+ let status = add_global_ids status s in
+ let status = add_name_for_reference status r s in
+ status,s
+ in
+ ref_renaming status (k,r)
+ in
+ let baseuri = Filename.dirname (NReference.string_of_reference r) in
+ if current_baseuri status = baseuri then
+ status,s
+ else
+ let modname = Filename.basename (Filename.dirname (NReference.string_of_reference r)) in
+ let status,modname = modname_of_filename status true modname in
+ status, modname ^ "." ^ s
+
+(* Main name printing function for a reference *)
+
+let pp_global status k r = ref_renaming status (k,r)
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+open Coq
+open Miniml
+open Mlutil
+open OcamlExtractionTable
+
+(** By default, in module Format, you can do horizontal placing of blocks
+ even if they include newlines, as long as the number of chars in the
+ blocks are less that a line length. To avoid this awkward situation,
+ we attach a big virtual size to [fnl] newlines. *)
+
+val fnl : unit -> std_ppcmds
+val fnl2 : unit -> std_ppcmds
+val space_if : bool -> std_ppcmds
+
+val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pr_binding : identifier list -> std_ppcmds
+
+type env = identifier list * Idset.t
+val empty_env : #OcamlExtractionTable.status -> env
+
+val fake_spec: NReference.spec
+
+val rename_tvars: Idset.t -> identifier list -> identifier list
+val push_vars : identifier list -> env -> identifier list * env
+val get_db_name : int -> env -> identifier
+
+(* true = capitalize *)
+val modname_of_filename: #status as 'status-> bool -> string -> 'status * string
+
+type kind = Term | Type | Cons
+
+val pp_global :
+ #status as 'status -> kind -> NReference.reference -> 'status * string
--- /dev/null
+type identifier = string
+
+(* Util.ml *)
+
+let is_digit c = (c >= '0' && c <= '9')
+
+(* Nameops.ml *)
+
+let has_subscript id =
+ is_digit (id.[String.length id - 1])
+
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
+let cut_ident skip_quote s =
+ let slen = String.length s in
+ (* [n'] is the position of the first non nullary digit *)
+ let rec numpart n n' =
+ if n = 0 then
+ (* ident made of _ and digits only [and ' if skip_quote]: don't cut it *)
+ slen
+ else
+ let c = Char.code (String.get s (n-1)) in
+ if c = code_of_0 && n <> slen then
+ numpart (n-1) n'
+ else if code_of_0 <= c && c <= code_of_9 then
+ numpart (n-1) (n-1)
+ else if skip_quote & (c = Char.code '\'' || c = Char.code '_') then
+ numpart (n-1) (n-1)
+ else
+ n'
+ in
+ numpart slen slen
+
+let forget_subscript id =
+ let numstart = cut_ident false id in
+ let newid = String.make (numstart+1) '0' in
+ String.blit id 0 newid 0 numstart;
+ newid
+
+(* Namegen.ml *)
+
+let restart_subscript id =
+ if not (has_subscript id) then id else
+ (* Ce serait sans doute mieux avec quelque chose inspiré de
+ *** make_ident id (Some 0) *** mais ça brise la compatibilité... *)
+ forget_subscript id
+
+(* Rem: semantics is a bit different, if an ident starts with toto00 then
+ after successive renamings it comes to toto09, then it goes on with toto10 *)
+let lift_subscript id =
+ let len = String.length id in
+ let rec add carrypos =
+ let c = id.[carrypos] in
+ if is_digit c then
+ if c = '9' then begin
+ assert (carrypos>0);
+ add (carrypos-1)
+ end
+ else begin
+ let newid = String.copy id in
+ String.fill newid (carrypos+1) (len-1-carrypos) '0';
+ newid.[carrypos] <- Char.chr (Char.code c + 1);
+ newid
+ end
+ else begin
+ let newid = id^"0" in
+ if carrypos < len-1 then begin
+ String.fill newid (carrypos+1) (len-1-carrypos) '0';
+ newid.[carrypos+1] <- '1'
+ end;
+ newid
+ end
+ in add (len-1)
+
+let next_ident_away_from id bad =
+ let rec name_rec id = if bad id then name_rec (lift_subscript id) else id in
+ name_rec id
+
+let next_ident_away id avoid =
+ if List.mem id avoid then
+ next_ident_away_from (restart_subscript id) (fun id -> List.mem id avoid)
+ else id
+
+(* ----- *)
+
+type label
+type reference
+
+type env
+type constant_body
+type ('a,'b) prec_declaration
+
+type module_path
+type mod_bound_id
+
+module Intmap = Map.Make(struct type t = int let compare = compare end)
+
+module Intset = Set.Make(struct type t = int let compare = compare end)
+
+module Idset = Set.Make(struct type t = identifier let compare = compare end)
+
+module Uriset = Set.Make(struct type t = NUri.uri let compare = NUri.compare end)
+
+module Refmap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
+
+module Stringmap = Map.Make(String)
+
+(* Pp_control.ml *)
+
+module Pp_control =
+ struct
+ let with_output_to _ = assert false
+ let get_margin _ = assert false
+ end
+
+(* Util.ml *)
+
+let list_map_i f =
+ let rec map_i_rec i = function
+ | [] -> []
+ | x::l -> let v = f i x in v :: map_i_rec (i+1) l
+ in
+ map_i_rec
+
+let list_map_i_status status f =
+ let rec map_i_rec status i = function
+ | [] -> status,[]
+ | x::l -> let status,v = f status i x in
+ let status,res = map_i_rec status (i+1) l in
+ status,v :: res
+ in
+ map_i_rec status
+
+let iterate f =
+ let rec iterate_f n x =
+ if n <= 0 then x else iterate_f (pred n) (f x)
+ in
+ iterate_f
+
+let rec list_skipn n l = match n,l with
+ | 0, _ -> l
+ | _, [] -> failwith "list_skipn"
+ | n, _::l -> list_skipn (pred n) l
+
+let list_split_at index l =
+ let rec aux i acc = function
+ tl when i = index -> (List.rev acc), tl
+ | hd :: tl -> aux (succ i) (hd :: acc) tl
+ | [] -> failwith "list_split_at: Invalid argument"
+ in aux 0 [] l
+
+let list_chop n l =
+ let rec chop_aux acc = function
+ | (0, l2) -> (List.rev acc, l2)
+ | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+ | (_, []) -> failwith "list_chop"
+ in
+ chop_aux [] (n,l)
+
+let list_firstn n l =
+ let rec aux acc = function
+ | (0, _l) -> List.rev acc
+ | (n, (h::t)) -> aux (h::acc) (pred n, t)
+ | _ -> failwith "firstn"
+ in
+ aux [] (n,l)
+
+let list_fold_left_i f =
+ let rec it_list_f i a = function
+ | [] -> a
+ | b::l -> it_list_f (i+1) (f i a b) l
+ in
+ it_list_f
+
+let list_iter_i f l = list_fold_left_i (fun i _ x -> f i x) 0 () l
+
+let list_lastn n l =
+ let len = List.length l in
+ let rec aux m l =
+ if m = n then l else aux (m - 1) (List.tl l)
+ in
+ if len < n then failwith "lastn" else aux len l
+
+let array_map2 f v1 v2 =
+ if Array.length v1 <> Array.length v2 then invalid_arg "array_map2";
+ if Array.length v1 == 0 then
+ [| |]
+ else begin
+ let res = Array.create (Array.length v1) (f v1.(0) v2.(0)) in
+ for i = 1 to pred (Array.length v1) do
+ res.(i) <- f v1.(i) v2.(i)
+ done;
+ res
+ end
+
+let array_for_all f v =
+ let rec allrec = function
+ | -1 -> true
+ | n -> (f v.(n)) && (allrec (n-1))
+ in
+ allrec ((Array.length v)-1)
+
+let array_fold_right_i f v a =
+ let rec fold a n =
+ if n=0 then a
+ else
+ let k = n-1 in
+ fold (f k v.(k) a) k in
+ fold a (Array.length v)
+
+let identity x = x
+
+let interval n m =
+ let rec interval_n (l,m) =
+ if n > m then l else interval_n (m::l,pred m)
+ in
+ interval_n ([],m)
+
+let map_status status f l =
+ List.fold_right
+ (fun x (status,res)->let status,y = f status x in status,y::res) l (status,[])
+
+(* CSC: Inefficiently implemented *)
+let array_map_status status f l =
+ let status,res = map_status status f (Array.to_list l) in
+ status,Array.of_list res
+
+(* CSC: Inefficiently implemented *)
+let array_mapi_status status f l =
+ let status,res = list_map_i_status status f 0 (Array.to_list l) in
+ status,Array.of_list res
+
+(* Pp.ml4 *)
+
+type block_type =
+ | Pp_hbox of int
+ | Pp_vbox of int
+ | Pp_hvbox of int
+ | Pp_hovbox of int
+ | Pp_tbox
+
+type 'a ppcmd_token =
+ | Ppcmd_print of 'a
+ | Ppcmd_box of block_type * ('a ppcmd_token Stream.t)
+ | Ppcmd_print_break of int * int
+ | Ppcmd_set_tab
+ | Ppcmd_print_tbreak of int * int
+ | Ppcmd_white_space of int
+ | Ppcmd_force_newline
+ | Ppcmd_print_if_broken
+ | Ppcmd_open_box of block_type
+ | Ppcmd_close_box
+ | Ppcmd_close_tbox
+ | Ppcmd_comment of int
+
+type ppcmd = (int*string) ppcmd_token
+
+type std_ppcmds = ppcmd Stream.t
+
+type 'a ppdir_token =
+ | Ppdir_ppcmds of 'a ppcmd_token Stream.t
+ | Ppdir_print_newline
+ | Ppdir_print_flush
+
+let utf8_length s =
+ let len = String.length s
+ and cnt = ref 0
+ and nc = ref 0
+ and p = ref 0 in
+ while !p < len do
+ begin
+ match s.[!p] with
+ | '\000'..'\127' -> nc := 0 (* ascii char *)
+ | '\128'..'\191' -> nc := 0 (* cannot start with a continuation byte *)
+ | '\192'..'\223' -> nc := 1 (* expect 1 continuation byte *)
+ | '\224'..'\239' -> nc := 2 (* expect 2 continuation bytes *)
+ | '\240'..'\247' -> nc := 3 (* expect 3 continuation bytes *)
+ | '\248'..'\251' -> nc := 4 (* expect 4 continuation bytes *)
+ | '\252'..'\253' -> nc := 5 (* expect 5 continuation bytes *)
+ | '\254'..'\255' -> nc := 0 (* invalid byte *)
+ end ;
+ incr p ;
+ while !p < len && !nc > 0 do
+ match s.[!p] with
+ | '\128'..'\191' (* next continuation byte *) -> incr p ; decr nc
+ | _ (* not a continuation byte *) -> nc := 0
+ done ;
+ incr cnt
+ done ;
+ !cnt
+
+let (++) = Stream.iapp
+let str s = [< 'Ppcmd_print (utf8_length s,s) >]
+let spc () = [< 'Ppcmd_print_break (1,0) >]
+let mt () = [< >]
+let v n s = [< 'Ppcmd_box(Pp_vbox n,s) >]
+let hv n s = [< 'Ppcmd_box(Pp_hvbox n,s) >]
+let hov n s = [< 'Ppcmd_box(Pp_hovbox n,s) >]
+let int n = str (string_of_int n)
+let stras (i,s) = [< 'Ppcmd_print (i,s) >]
+let fnl () = [< 'Ppcmd_force_newline >]
+
+let com_eol = ref false
+
+let com_brk _ft = com_eol := false
+let com_if ft f =
+ if !com_eol then (com_eol := false; Format.pp_force_newline ft ())
+ else Lazy.force f
+
+let comments = ref []
+
+let rec split_com comacc acc pos = function
+ [] -> comments := List.rev acc; comacc
+ | ((b,e),c as com)::coms ->
+ (* Take all comments that terminates before pos, or begin exactly
+ at pos (used to print comments attached after an expression) *)
+ if e<=pos || pos=b then split_com (c::comacc) acc pos coms
+ else split_com comacc (com::acc) pos coms
+
+let rec pr_com ft s =
+ let (s1,os) =
+ try
+ let n = String.index s '\n' in
+ String.sub s 0 n, Some (String.sub s (n+1) (String.length s - n - 1))
+ with Not_found -> s,None in
+ com_if ft (Lazy.lazy_from_val());
+(* let s1 =
+ if String.length s1 <> 0 && s1.[0] = ' ' then
+ (Format.pp_print_space ft (); String.sub s1 1 (String.length s1 - 1))
+ else s1 in*)
+ Format.pp_print_as ft (utf8_length s1) s1;
+ match os with
+ Some s2 ->
+ if String.length s2 = 0 then (com_eol := true)
+ else
+ (Format.pp_force_newline ft (); pr_com ft s2)
+ | None -> ()
+
+let pp_dirs ft =
+ let pp_open_box = function
+ | Pp_hbox _n -> Format.pp_open_hbox ft ()
+ | Pp_vbox n -> Format.pp_open_vbox ft n
+ | Pp_hvbox n -> Format.pp_open_hvbox ft n
+ | Pp_hovbox n -> Format.pp_open_hovbox ft n
+ | Pp_tbox -> Format.pp_open_tbox ft ()
+ in
+ let rec pp_cmd = function
+ | Ppcmd_print(n,s) ->
+ com_if ft (Lazy.lazy_from_val()); Format.pp_print_as ft n s
+ | Ppcmd_box(bty,ss) -> (* Prevent evaluation of the stream! *)
+ com_if ft (Lazy.lazy_from_val());
+ pp_open_box bty ;
+ if not (Format.over_max_boxes ()) then Stream.iter pp_cmd ss;
+ Format.pp_close_box ft ()
+ | Ppcmd_open_box bty -> com_if ft (Lazy.lazy_from_val()); pp_open_box bty
+ | Ppcmd_close_box -> Format.pp_close_box ft ()
+ | Ppcmd_close_tbox -> Format.pp_close_tbox ft ()
+ | Ppcmd_white_space n ->
+ com_if ft (Lazy.lazy_from_fun (fun()->Format.pp_print_break ft n 0))
+ | Ppcmd_print_break(m,n) ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_break ft m n))
+ | Ppcmd_set_tab -> Format.pp_set_tab ft ()
+ | Ppcmd_print_tbreak(m,n) ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_tbreak ft m n))
+ | Ppcmd_force_newline ->
+ com_brk ft; Format.pp_force_newline ft ()
+ | Ppcmd_print_if_broken ->
+ com_if ft (Lazy.lazy_from_fun(fun()->Format.pp_print_if_newline ft ()))
+ | Ppcmd_comment i ->
+ let coms = split_com [] [] i !comments in
+(* Format.pp_open_hvbox ft 0;*)
+ List.iter (pr_com ft) coms(*;
+ Format.pp_close_box ft ()*)
+ in
+ let pp_dir = function
+ | Ppdir_ppcmds cmdstream -> Stream.iter pp_cmd cmdstream
+ | Ppdir_print_newline ->
+ com_brk ft; Format.pp_print_newline ft ()
+ | Ppdir_print_flush -> Format.pp_print_flush ft ()
+ in
+ fun dirstream ->
+ try
+ Stream.iter pp_dir dirstream; com_brk ft
+ with
+ | e -> Format.pp_print_flush ft () ; raise e
+
+let pp_with ft strm =
+ pp_dirs ft [< 'Ppdir_ppcmds strm >]
+
+(* Util.ml *)
+
+let rec prlist_with_sep sep elem l = match l with
+ | [] -> mt ()
+ | [h] -> elem h
+ | h::t ->
+ let e = elem h and s = sep() and r = prlist_with_sep sep elem t in
+ e ++ s ++ r
+
+let rec prlist_with_sep_status status sep elem l = match l with
+ | [] -> status,mt ()
+ | [h] -> elem status h
+ | h::t ->
+ let status,e = elem status h in
+ let s = sep() in
+ let status,r = prlist_with_sep_status status sep elem t in
+ status, e ++ s ++ r
+
+let rec prlist elem l = match l with
+ | [] -> mt ()
+ | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
+
+let rec prlist_strict elem l = match l with
+ | [] -> mt ()
+ | h::t ->
+ let e = elem h in let r = prlist_strict elem t in e++r
+
+let prvecti_with_sep sep elem v =
+ let rec pr i =
+ if i = 0 then
+ elem 0 v.(0)
+ else
+ let r = pr (i-1) and s = sep () and e = elem i v.(i) in
+ r ++ s ++ e
+ in
+ let n = Array.length v in
+ if n = 0 then mt () else pr (n - 1)
+
+let prvecti_with_sep_status status sep elem v =
+ let rec pr status i =
+ if i = 0 then
+ elem status 0 v.(0)
+ else
+ let status,r = pr status (i-1) in
+ let s = sep () in
+ let status,e = elem status i v.(i) in
+ status, r ++ s ++ e
+ in
+ let n = Array.length v in
+ if n = 0 then status,mt () else pr status (n - 1)
+
+let prvecti elem v = prvecti_with_sep mt elem v
+
+let prvecti_status status elem v = prvecti_with_sep_status status mt elem v
+
+let prvect_with_sep sep elem v = prvecti_with_sep sep (fun _ -> elem) v
+
+let prvect_with_sep_status status sep elem v =
+ prvecti_with_sep_status status sep (fun status _ -> elem status) v
+
+let prvect elem v = prvect_with_sep mt elem v
+
+(* Nameops.ml *)
+
+let pr_id id = str id
+
+(* ---- *)
--- /dev/null
+type identifier = string
+
+val next_ident_away : identifier -> identifier list -> identifier
+
+val lift_subscript : identifier -> identifier
+
+type label
+type reference
+
+type env
+type constant_body
+type ('a,'b) prec_declaration
+
+type module_path
+type mod_bound_id
+
+module Intmap : Map.S with type key = int
+
+module Intset : Set.S with type elt = int
+
+module Uriset : Set.S with type elt = NUri.uri
+
+module Idset : Set.S with type elt=identifier
+
+module Refmap : Map.S with type key = NReference.reference
+
+module Stringmap : Map.S with type key = string
+
+module Pp_control : sig
+ val with_output_to : out_channel -> Format.formatter
+ val get_margin: unit -> int option
+end
+
+val iterate : ('a -> 'a) -> int -> 'a -> 'a
+val list_skipn : int -> 'a list -> 'a list
+val list_split_at : int -> 'a list -> 'a list*'a list
+val list_chop : int -> 'a list -> 'a list * 'a list
+val list_firstn : int -> 'a list -> 'a list
+val list_iter_i : (int -> 'a -> unit) -> 'a list -> unit
+val list_lastn : int -> 'a list -> 'a list
+val array_map2 : ('a -> 'b -> 'c) -> 'a array -> 'b array -> 'c array
+val array_for_all : ('a -> bool) -> 'a array -> bool
+val array_fold_right_i :
+ (int -> 'b -> 'a -> 'a) -> 'b array -> 'a -> 'a
+val identity : 'a -> 'a
+val interval : int -> int -> int list
+val map_status: 's -> ('s -> 'a -> 's * 'b) -> 'a list -> 's * 'b list
+val array_map_status: 's -> ('s -> 'a -> 's * 'b) -> 'a array -> 's * 'b array
+val array_mapi_status :
+ 's -> ('s -> int -> 'a -> 's * 'b) -> 'a array -> 's * 'b array
+
+type std_ppcmds
+val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds
+val spc : unit -> std_ppcmds
+val str : string -> std_ppcmds
+val mt : unit -> std_ppcmds
+val v : int -> std_ppcmds -> std_ppcmds
+val hv : int -> std_ppcmds -> std_ppcmds
+val hov : int -> std_ppcmds -> std_ppcmds
+val int : int -> std_ppcmds
+val stras : int * string -> std_ppcmds
+val fnl : unit -> std_ppcmds
+val prlist_with_sep_status :
+ 'a -> (unit -> std_ppcmds) -> ('a -> 'b -> 'a * std_ppcmds) -> 'b list ->
+ 'a * std_ppcmds
+val prlist_with_sep :
+ (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
+val pr_id : identifier -> std_ppcmds
+val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val prvect_with_sep :
+ (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvect_with_sep_status :
+ 's -> (unit -> std_ppcmds) -> ('s -> 'a -> 's * std_ppcmds) -> 'a array -> 's * std_ppcmds
+val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
+val prvecti_status :
+ 's -> ('s -> int -> 'a -> 's * std_ppcmds) -> 'a array -> 's * std_ppcmds
+val list_map_i : (int -> 'a -> 'b) -> int -> 'a list -> 'b list
+val list_map_i_status :
+ 's -> ('s -> int -> 'a -> 's * 'b) -> int -> 'a list -> 's * 'b list
+
+val pp_with : Format.formatter -> std_ppcmds -> unit
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: extraction.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
+
+open Coq
+open Miniml
+open OcamlExtractionTable
+open Mlutil
+open Common
+
+(* A set of all fixpoint functions currently being extracted *)
+(*CSC: very imperative, fix/check?*)
+let current_fixpoints = ref (None : NUri.uri option)
+
+let whd_betadeltaiota status context t =
+ NCicReduction.whd status ~subst:[] context t
+
+let whd_betaiotazeta status context t =
+ NCicReduction.whd status ~delta:max_int ~subst:[] context t
+
+let isRel = function NCic.Rel _ -> true | _ -> false
+
+let rec split_all_prods status ~subst context te =
+ match NCicReduction.whd status ~subst context te with
+ | NCic.Prod (name,so,ta) ->
+ split_all_prods status ~subst ((name,(NCic.Decl so))::context) ta
+ | _ -> context,te
+;;
+
+(* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
+ * gives n *)
+let nb_lam =
+ let rec nbrec n =
+ function
+ | NCic.Lambda (_,_,c) -> nbrec (n+1) c
+ | _ -> n
+ in
+ nbrec 0
+
+(* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
+ into the pair ([(xn,Tn);...;(x1,T1)],T) *)
+let decompose_lam_n n =
+ if n < 0 then assert false else
+ let rec lamdec_rec l n c =
+ if n=0 then l,c
+ else match c with
+ | NCic.Lambda (x,t,c) -> lamdec_rec ((x,NCic.Decl t)::l) (n-1) c
+ | _ -> assert false
+ in
+ lamdec_rec [] n
+
+let decompose_lam =
+ let rec lamdec_rec l =
+ function
+ | NCic.Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
+ | c -> l,c
+ in
+ lamdec_rec []
+
+let splay_prod_n status context n =
+ let rec decrec context m ln c = if m = 0 then (ln,c) else
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,a,c0) ->
+ decrec ((n,NCic.Decl a)::context)
+ (m-1) ((n,NCic.Decl a)::ln) c0
+ | _ -> invalid_arg "splay_prod_n"
+ in
+ decrec context n []
+
+let splay_prod status context =
+ let rec decrec context m c =
+ let t = whd_betadeltaiota status context c in
+ match t with
+ | NCic.Prod (n,a,c0) ->
+ decrec ((n,NCic.Decl a)::context) ((n,NCic.Decl a)::m) c0
+ | _ -> m,t
+ in
+ decrec context []
+
+let type_of status context t =
+ NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
+
+type sorts_family = InProp | InType
+
+let classify_sort =
+ function
+ NCic.Prop -> InProp
+ | NCic.Type u ->
+ match NCicEnvironment.family_of u with
+ `CProp -> InProp
+ | `Type -> InType
+
+let sort_of status context t =
+ match
+ NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
+ with
+ NCic.Sort s -> classify_sort s
+ | _ -> assert false
+
+(*S Generation of flags and signatures. *)
+
+(* The type [flag] gives us information about any Coq term:
+ \begin{itemize}
+ \item [TypeScheme] denotes a type scheme, that is
+ something that will become a type after enough applications.
+ More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
+ [s = Set], [Prop] or [Type]
+ \item [Default] denotes the other cases. It may be inexact after
+ instanciation. For example [(X:Type)X] is [Default] and may give [Set]
+ after instanciation, which is rather [TypeScheme]
+ \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
+ \item [Info] is the opposite. The same example [(X:Type)X] shows
+ that an [Info] term might in fact be [Logic] later on.
+ \end{itemize} *)
+
+type info = Logic | Info
+
+type scheme = TypeScheme | Default
+
+type flag = info * scheme
+
+(*s [flag_of_type] transforms a type [t] into a [flag].
+ Really important function. *)
+
+let rec flag_of_type status context t =
+ let t = whd_betadeltaiota status context t in
+ match t with
+ | NCic.Prod (x,t,c) -> flag_of_type status ((x,NCic.Decl t)::context) c
+ | NCic.Sort s ->
+ (match classify_sort s with
+ InProp -> (Logic,TypeScheme)
+ | InType -> (Info,TypeScheme))
+ | _ ->
+ if (sort_of status context t) = InProp then (Logic,Default)
+ else (Info,Default)
+
+(*s Two particular cases of [flag_of_type]. *)
+
+let is_default status context t=(flag_of_type status context t= (Info, Default))
+
+exception NotDefault of kill_reason
+
+let check_default status context t =
+ match flag_of_type status context t with
+ | _,TypeScheme -> raise (NotDefault Ktype)
+ | Logic,_ -> raise (NotDefault Kother)
+ | _ -> ()
+
+let is_info_scheme status context t =
+ (flag_of_type status context t = (Info, TypeScheme))
+
+(*s [type_sign] generates a signature aimed at treating a type application. *)
+
+let rec type_sign status context c =
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,t,d) ->
+ (if is_info_scheme status context t then Keep else Kill Kother)
+ :: (type_sign status ((n,NCic.Decl t)::context) d)
+ | _ -> []
+
+let rec type_scheme_nb_args status context c =
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,t,d) ->
+ let n = type_scheme_nb_args status ((n,NCic.Decl t)::context) d in
+ if is_info_scheme status context t then n+1 else n
+ | _ -> 0
+
+(*CSC: only useful for inline extraction
+let _ = register_type_scheme_nb_args type_scheme_nb_args
+*)
+
+(*s [type_sign_vl] does the same, plus a type var list. *)
+
+let rec type_sign_vl status context c =
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,t,d) ->
+ let s,vl = type_sign_vl status ((n,NCic.Decl t)::context) d in
+ if not (is_info_scheme status context t) then Kill Kother::s, vl
+ else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
+ | _ -> [],[]
+
+let rec nb_default_params status context c =
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,t,d) ->
+ let n = nb_default_params status ((n,NCic.Decl t)::context) d in
+ if is_default status context t then n+1 else n
+ | _ -> 0
+
+(* Enriching a signature with implicit information *)
+
+let sign_with_implicits _r s =
+ let implicits = [](*CSC: implicits_of_global r*) in
+ let rec add_impl i = function
+ | [] -> []
+ | sign::s ->
+ let sign' =
+ if sign = Keep && List.mem i implicits then Kill Kother else sign
+ in sign' :: add_impl (succ i) s
+ in
+ add_impl 1 s
+
+(* Enriching a exception message *)
+
+let rec handle_exn _r _n _fn_name = function x -> x
+(*CSC: only for pretty printing
+ | 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 _ -> 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]
+ into ML type [Tvar]. *)
+
+(*s From a type signature toward a type variable context (db). *)
+
+let db_from_sign s =
+ let rec make i acc = function
+ | [] -> acc
+ | Keep :: l -> make (i+1) (i::acc) l
+ | Kill _ :: l -> make i (0::acc) l
+ in make 1 [] s
+
+(*s Create a type variable context from indications taken from
+ an inductive type (see just below). *)
+
+let rec db_from_ind dbmap i =
+ if i = 0 then []
+ else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
+
+(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
+ of a constructor corresponds to the j-th type var of the ML inductive. *)
+
+(* \begin{itemize}
+ \item [si] : signature of the inductive
+ \item [i] : counter of Coq args for [(I args)]
+ \item [j] : counter of ML type vars
+ \item [relmax] : total args number of the constructor
+ \end{itemize} *)
+
+let parse_ind_args si args relmax =
+ let rec parse i j = function
+ | [] -> Intmap.empty
+ | Kill _ :: s -> parse (i+1) j s
+ | Keep :: s ->
+ (match args.(i-1) with
+ | NCic.Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
+ | _ -> parse (i+1) (j+1) s)
+ in parse 1 1 si
+
+(*S Extraction of a type. *)
+
+(* [extract_type env db c args] is used to produce an ML type from the
+ coq term [(c args)], which is supposed to be a Coq type. *)
+
+(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
+
+(* [j] stands for the next ML type var. [j=0] means we do not
+ generate ML type var anymore (in subterms for example). *)
+
+
+let rec extract_type status context db j c args =
+ match whd_betaiotazeta status context c with
+ | NCic.Appl (d::args') ->
+ (* We just accumulate the arguments. *)
+ extract_type status context db j d (args' @ args)
+ | NCic.Lambda (_,_,d) ->
+ (match args with
+ | [] -> assert false (* otherwise the lambda would be reductible. *)
+ | a :: args -> extract_type status context db j (NCicSubstitution.subst status a d) args)
+ | NCic.Prod (n,t,d) ->
+ assert (args = []);
+ let context' = (n,NCic.Decl t)::context in
+ (match flag_of_type status context t with
+ | (Info, Default) ->
+ (* Standard case: two [extract_type] ... *)
+ let status,mld = extract_type status context' (0::db) j d [] in
+ let status,res = expand status mld in
+ (match res with
+ | Tdummy d -> status,Tdummy d
+ | _ ->
+ let status,res=extract_type status context db 0 t [] in
+ status,Tarr (res, mld))
+ | (Info, TypeScheme) when j > 0 ->
+ (* A new type var. *)
+ let status,mld=extract_type status context' (j::db) (j+1) d [] in
+ let status,res = expand status mld in
+ status,
+ (match res with
+ | Tdummy d -> Tdummy d
+ | _ -> Tarr (Tdummy Ktype, mld))
+ | _,lvl ->
+ let status,mld = extract_type status context' (0::db) j d [] in
+ let status,res = expand status mld in
+ status,
+ (match res with
+ | Tdummy d -> Tdummy d
+ | _ ->
+ let reason = if lvl=TypeScheme then Ktype else Kother in
+ Tarr (Tdummy reason, mld)))
+ | NCic.Sort _ -> status,Tdummy Ktype (* The two logical cases. *)
+ | _ when sort_of status context (NCicUntrusted.mk_appl c args) = InProp ->
+ status,Tdummy Kother
+ | NCic.Rel n ->
+ (match List.nth context (n-1) with
+ | (_,NCic.Def (t,_)) -> extract_type status context db j (NCicSubstitution.lift status n t) args
+ | _ ->
+ (* Asks [db] a translation for [n]. *)
+ if n > List.length db then status,Tunknown
+ else let n' = List.nth db (n-1) in
+ status,if n' = 0 then Tunknown else Tvar n')
+ | NCic.Const (NReference.Ref (uri,spec) as r) ->
+ (match spec with
+ NReference.Decl ->
+ let _,_,typ,_,_ = NCicEnvironment.get_checked_decl status r in
+ (match flag_of_type status [] typ with
+ | (Info, TypeScheme) ->
+ extract_type_app status context db
+ (r, type_sign status [] typ) args
+ | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
+ status,Tunknown (* Brutal approximation ... *))
+ | NReference.Def _ ->
+ let _,_,bo,typ,_,_ = NCicEnvironment.get_checked_def status r in
+ (match flag_of_type status [] typ with
+ | (Info, TypeScheme) ->
+ let status,mlt =
+ extract_type_app status context db
+ (r, type_sign status [] typ) args in
+ (*CSC: if is_custom r then mlt else*)
+ let newc = NCicUntrusted.mk_appl bo args in
+ let status,mlt' = extract_type status context db j newc [] in
+ (* ML type abbreviations interact badly with Coq *)
+ (* reduction, so [mlt] and [mlt'] might be different: *)
+ (* The more precise is [mlt'], extracted after reduction *)
+ (* The shortest is [mlt], which use abbreviations *)
+ (* If possible, we take [mlt], otherwise [mlt']. *)
+ let status,res1 = expand status mlt in
+ let status,res2 = expand status mlt' in
+ if res1=res2 then status,mlt else status,mlt'
+ | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
+ (* We try to reduce. *)
+ let newc = NCicUntrusted.mk_appl bo args in
+ extract_type status context db j newc [])
+ | NReference.Fix _ -> status,Tunknown
+ | NReference.Con _
+ | NReference.CoFix _ -> assert false
+ | NReference.Ind (_,i,_) ->
+ let status,ind = extract_ind status uri in
+ let s = ind.ind_packets.(i).ip_sign in
+ extract_type_app status context db (r,s) args)
+ | NCic.Match _ -> status,Tunknown
+ | _ -> assert false
+
+(*s Auxiliary function dealing with type application.
+ Precondition: [r] is a type scheme represented by the signature [s],
+ and is completely applied: [List.length args = List.length s]. *)
+
+and extract_type_app status context db (r,s) args =
+ let status,ml_args =
+ List.fold_right
+ (fun (b,c) (status,a) ->
+ if b=Keep then
+ let p =
+ List.length
+ (fst (splay_prod status context (type_of status context c))) in
+ let db = iterate (fun l -> 0 :: l) p db in
+ let status,res = extract_type_scheme status context db c p in
+ status,res::a
+ else status,a)
+ (List.combine s args) (status,[])
+ in status, Tglob (r, ml_args)
+
+(*S Extraction of a type scheme. *)
+
+(* [extract_type_scheme env db c p] works on a Coq term [c] which is
+ an informative type scheme. It means that [c] is not a Coq type, but will
+ be when applied to sufficiently many arguments ([p] in fact).
+ This function decomposes p lambdas, with eta-expansion if needed. *)
+
+(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
+
+and extract_type_scheme status context db c p =
+ if p=0 then extract_type status context db 0 c []
+ else
+ let c = whd_betaiotazeta status context c in
+ match c with
+ | NCic.Lambda (n,t,d) ->
+ extract_type_scheme status((n,NCic.Decl t)::context) db d (p-1)
+ | _ ->
+ let rels=fst (splay_prod status context (type_of status context c)) in
+ let context = rels@context in
+ let eta_args = List.rev_map (fun x -> NCic.Rel x) (interval 1 p) in
+ extract_type status context db 0 (NCicSubstitution.lift status p c)
+ eta_args
+
+
+(*S Extraction of an inductive type. *)
+
+and extract_ind status uri =
+ try
+ status,lookup_ind status uri
+ with Not_found ->
+ let _,_,_,_,obj = NCicEnvironment.get_checked_obj status uri in
+ match obj with
+ NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
+ extract_ind0 status uri inductive ind_pragma leftno types
+ | _ -> assert false
+
+and extract_ind0 status uri inductive ind_pragma leftno types =
+ (* First, if this inductive is aliased via a Module, *)
+ (* we process the original inductive. *)
+ (* Everything concerning parameters. *)
+ (* We do that first, since they are common to all the [mib]. *)
+ let _,_,mipty0,_ = List.hd types in
+ let mipcontext,_=NCicReduction.split_prods status ~subst:[] [] ~-1 mipty0 in
+ let epar_rev,_= HExtlib.split_nth leftno (List.rev mipcontext) in
+ let epar = List.rev epar_rev in
+ (* First pass: we store inductive signatures together with *)
+ (* their type var list. *)
+ let packets =
+ Array.mapi
+ (fun tyno (_,name,arity,kl) ->
+ let _,sort=NCicReduction.split_prods status ~subst:[] [] ~-1 arity in
+ let sort=match sort with NCic.Sort sort -> sort | _ ->assert false in
+ let b = classify_sort sort <> InProp in
+ let s,v = if b then type_sign_vl status [] arity else [],[] in
+ let t = Array.make (List.length kl) [] in
+ let kl = Array.of_list kl in
+ let spec = NReference.Ind (inductive,tyno,leftno) in
+ let ref = NReference.reference_of_spec uri spec in
+ { ip_reference = ref;
+ ip_consreferences =
+ Array.mapi
+ (fun i _ ->
+ NReference.reference_of_spec uri
+ (NReference.Con (tyno,i+1,leftno))
+ ) kl;
+ ip_typename = name;
+ ip_consnames= Array.map (fun (_,name,_) -> name) kl;
+ ip_logical = (not b);
+ ip_sign = s;
+ ip_vars = v;
+ ip_types = t
+ })
+ (Array.of_list types)
+ in
+ let status = add_ind ~dummy:true status uri
+ {ind_kind = Standard;
+ ind_nparams = leftno;
+ ind_packets = packets
+ } in
+ (* Second pass: we extract constructors *)
+ let rec aux1 i status =
+ if i = List.length types then status
+ else begin
+ let p = packets.(i) in
+ let _,_,_,cl = List.nth types i in
+ if not p.ip_logical then
+ let ktypes = Array.of_list (List.map (fun (_,_,arity) -> arity) cl) in
+ let rec aux2 j status =
+ if j = Array.length ktypes then status
+ else begin
+ let tctx,t =
+ NCicReduction.split_prods status ~subst:[] [] leftno ktypes.(j) in
+ let prods,head = split_all_prods status ~subst:[] tctx t in
+ let nprods = List.length prods in
+ let args = match head with
+ | NCic.Appl (_f::args) -> Array.of_list args (* [f = Ind ip] *)
+ | _ -> [||]
+ in
+ let dbmap = parse_ind_args p.ip_sign args nprods in
+ let db = db_from_ind dbmap leftno in
+ let status,res = extract_type_cons status epar db dbmap t (leftno+1)in
+ p.ip_types.(j) <- res;
+ aux2 (j+1) status
+ end
+ in
+ let status = aux2 0 status in
+ aux1 (i+1) status
+ else begin
+ aux1 (i+1) status
+ end
+ end in
+ let status = aux1 0 status in
+ (* Third pass: we determine special cases. *)
+ let status,ind_info =
+ (*CSC: let ip = (kn, 0) in
+ let r = IndRef ip in
+ if is_custom r then raise_I status Standard;*)
+ if not inductive then status,Coinductive else
+ if List.length types <> 1 then status,Standard else
+ let p = packets.(0) in
+ if p.ip_logical then status,Standard else
+ if Array.length p.ip_types <> 1 then status,Standard else
+ let typ = p.ip_types.(0) in
+ let status,l =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = expand status x in
+ status,y::res
+ ) typ (status,[]) in
+ let l = List.filter (fun t -> not (isDummy t)) l in
+ if List.length l = 1 && not (type_mem_kn uri (List.hd l))
+ then status,Singleton else
+ if l = [] then status,Standard else
+ (match ind_pragma with
+ `Regular -> status,Standard
+ | `Record fields ->
+ let baseuri = NUri.baseuri_of_uri uri in
+ let field_names = List.map (fun (n,_,_) -> n) fields in
+ assert (List.length field_names = List.length typ);
+ let rec select_fields status l typs = match l,typs with
+ | [],[] -> status,[]
+ | id::l, typ::typs ->
+ let status,res = expand status typ in
+ if isDummy res then
+ select_fields status l typs
+ else
+ (* Is it safe to use [id] for projections [foo.id] ? *)
+ let status,res = type2signature status typ in
+ let fielduri =
+ NUri.uri_of_string (baseuri ^ "/" ^ id ^ ".con") in
+ let fieldfakeref =
+ NReference.reference_of_spec fielduri fake_spec in
+(*
+ let ref =
+ try
+ let fieldspec =
+ let (_,height,_,_,obj) =
+ NCicEnvironment.get_checked_obj status fielduri
+ in
+ match obj with
+ NCic.Fixpoint (_,fs,(_,_,`Projection)) ->
+ let _,_,recparamno,_,_ = List.nth fs 0 in
+ NReference.Fix (0,recparamno,height)
+ | _ -> assert false
+ in
+ NReference.reference_of_spec fielduri fieldspec
+ with NCicEnvironment.ObjectNotFound _ ->
+ assert false
+ in *)
+ let status =
+ if List.for_all ((=) Keep) res
+ then
+ let n = nb_default_params status [] mipty0 in
+ guess_projection status fielduri n
+ else status in
+ let status,res = select_fields status l typs in
+ status, fieldfakeref::res
+ | _ -> assert false
+ in
+ let status,field_glob = select_fields status field_names typ in
+ (* Is this record officially declared with its projections ? *)
+ (* If so, we use this information. *)
+ status, Record field_glob)
+ in
+ let i = {ind_kind = ind_info;
+ ind_nparams = leftno;
+ ind_packets = packets
+ } in
+ let status = add_ind status uri i in
+ status,i
+
+(*s [extract_type_cons] extracts the type of an inductive
+ constructor toward the corresponding list of ML types.
+
+ - [db] is a context for translating Coq [Rel] into ML type [Tvar]
+ - [dbmap] is a translation map (produced by a call to [parse_in_args])
+ - [i] is the rank of the current product (initially [params_nb+1])
+*)
+
+and extract_type_cons status context db dbmap c i =
+ match whd_betadeltaiota status context c with
+ | NCic.Prod (n,t,d) ->
+ let context' = (n,NCic.Decl t)::context in
+ let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
+ let status,l = extract_type_cons status context' db' dbmap d (i+1) in
+ let status, res = extract_type status context db 0 t [] in
+ status, res::l
+ | _ -> status,[]
+
+(*s Recording the ML type abbreviation of a Coq type scheme constant. *)
+
+and mlt_env status r =
+ try
+ if false (*CSC:XXX not (visible_con kn)*) then raise Not_found;
+ match lookup_term status r with
+ | Dtype (_,_vl,mlt) -> Some (status,mlt)
+ | _ -> None
+ with Not_found ->
+ match r with
+ NReference.Ref (_,NReference.Def _) ->
+ let _,_,body,typ,_,_ = NCicEnvironment.get_checked_def status r in
+ (match flag_of_type status [] typ with
+ | Info,TypeScheme ->
+ let s,vl = type_sign_vl status [] typ in
+ let db = db_from_sign s in
+ let status,t =
+ extract_type_scheme status [] db body (List.length s) in
+ let status = add_term status r (Dtype (r, vl, t)) in
+ Some (status,t)
+ | _ -> None)
+ | NReference.Ref (_,NReference.Decl) -> None
+ | NReference.Ref (_,NReference.Fix _)
+ | NReference.Ref (_,NReference.CoFix _) -> assert false
+ | NReference.Ref (_,NReference.Ind _)
+ | NReference.Ref (_,NReference.Con _) -> None
+
+and expand status = type_expand status mlt_env
+and type2signature status = type_to_signature status mlt_env
+let type2sign status = type_to_sign status mlt_env
+let type_expunge status = type_expunge status mlt_env
+let type_expunge_from_sign status = type_expunge_from_sign status mlt_env
+
+(*s Extraction of the type of a constant. *)
+
+let type_of_constant status (NReference.Ref (uri,spec)) =
+ let (_,_,_,_,obj) = NCicEnvironment.get_checked_obj status uri in
+ match obj,spec with
+ NCic.Constant (_,_,_,typ,_),_ -> typ
+ | NCic.Fixpoint (_,fs,_), (NReference.Fix (n,_,_) | NReference.CoFix n) ->
+ let _,_,_,typ,_ = List.nth fs n in
+ typ
+ | _ -> assert false
+
+let record_constant_type status r opt_typ =
+ try
+(*CSC:XXX to be implemented? if not (visible_con kn) then raise Not_found;*)
+ status,lookup_type status r
+ with Not_found ->
+ let typ = match opt_typ with
+ | None -> type_of_constant status r
+ | Some typ -> typ in
+ let status,mlt = extract_type status [] [] 1 typ [] in
+ let schema = (type_maxvar mlt, mlt) in
+ let status = add_type status r schema in
+ status,schema
+
+(*S Extraction of a term. *)
+
+(* Precondition: [(c args)] is not a type scheme, and is informative. *)
+
+(* [mle] is a ML environment [Mlenv.t]. *)
+(* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
+
+let rec extract_term status context mle mlt c args =
+ match c with
+ NCic.Appl [] -> assert false
+ | NCic.Appl (f::a) ->
+ extract_term status context mle mlt f (a@args)
+ | NCic.Lambda (n, t, d) ->
+ let id = n in
+ (match args with
+ | a :: l ->
+ (* We make as many [LetIn] as possible. *)
+ let d' = NCic.LetIn (id,t,a,NCic.Appl (d::(List.map (NCicSubstitution.lift status 1) l)))
+ in extract_term status context mle mlt d' []
+ | [] ->
+ let context' = (id, NCic.Decl t)::context in
+ let id, a =
+ try check_default status context t; Id id, new_meta()
+ with NotDefault d -> Dummy, Tdummy d
+ in
+ let b = new_meta () in
+ (* If [mlt] cannot be unified with an arrow type, then magic! *)
+ let magic = needs_magic (mlt, Tarr (a, b)) in
+ let status,d' =
+ extract_term status context' (Mlenv.push_type mle a) b d [] in
+ status,put_magic_if magic (MLlam (id, d')))
+ | NCic.LetIn (n, t1, c1, c2) ->
+ let id = n in
+ let context' = (id, NCic.Def (c1, t1))::context in
+ let args' = List.map (NCicSubstitution.lift status 1) args in
+ (try
+ check_default status context t1;
+ let a = new_meta () in
+ let status,c1' = extract_term status context mle a c1 [] in
+ (* The type of [c1'] is generalized and stored in [mle]. *)
+ let mle' =
+ if generalizable c1'
+ then Mlenv.push_gen mle a
+ else Mlenv.push_type mle a
+ in
+ let status,res = extract_term status context' mle' mlt c2 args' in
+ status,MLletin (Id id, c1', res)
+ with NotDefault d ->
+ let mle' = Mlenv.push_std_type mle (Tdummy d) in
+ let status,res = extract_term status context' mle' mlt c2 args' in
+ status,ast_pop res)
+ | NCic.Const ((NReference.Ref (uri,
+ ( NReference.Decl
+ | NReference.Def _
+ | NReference.Fix _
+ | NReference.CoFix _ ))) as ref) ->
+ extract_cst_app status context mle mlt uri ref args
+ | NCic.Const ((NReference.Ref (_,(NReference.Con _))) as ref) ->
+ extract_cons_app status context mle mlt ref args
+ | NCic.Rel n ->
+ (* As soon as the expected [mlt] for the head is known, *)
+ (* we unify it with an fresh copy of the stored type of [Rel n]. *)
+ let extract_rel status mlt =
+ status,put_magic (mlt, Mlenv.get mle n) (MLrel n)
+ in extract_app status context mle mlt extract_rel args
+ | NCic.Match (ref,_,c0,br) ->
+ extract_app status context mle mlt
+ (extract_case context mle (ref,c0,Array.of_list br)) args
+ | NCic.Const (NReference.Ref (_,NReference.Ind _))
+ | NCic.Prod _
+ | NCic.Sort _
+ | NCic.Implicit _
+ | NCic.Meta _ -> assert false
+
+(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
+
+and extract_maybe_term status context mle mlt c =
+ try check_default status context (type_of status context c);
+ extract_term status context mle mlt c []
+ with NotDefault d ->
+ status,put_magic (mlt, Tdummy d) MLdummy
+
+(*s Generic way to deal with an application. *)
+
+(* We first type all arguments starting with unknown meta types.
+ This gives us the expected type of the head. Then we use the
+ [mk_head] to produce the ML head from this type. *)
+
+and extract_app status context mle mlt mk_head args =
+ let metas = List.map new_meta args in
+ let type_head = type_recomp (metas, mlt) in
+ let status,mlargs =
+ List.fold_right2
+ (fun x y (status,res) ->
+ let status,z = extract_maybe_term status context mle x y in
+ status,z::res
+ ) metas args (status,[]) in
+ let status,res = mk_head status type_head in
+ status,mlapp res mlargs
+
+(*s Auxiliary function used to extract arguments of constant or constructor. *)
+
+and make_mlargs status context e s args typs =
+ let rec f status = function
+ | [], [], _ -> status,[]
+ | a::la, t::lt, [] ->
+ let status,res = extract_maybe_term status context e t a in
+ let status,res2 = f status (la,lt,[]) in
+ status, res :: res2
+ | a::la, t::lt, Keep::s ->
+ let status,res = extract_maybe_term status context e t a in
+ let status,res2 = f status (la,lt,s) in
+ status, res :: res2
+ | _::la, _::lt, _::s -> f status (la,lt,s)
+ | _ -> assert false
+ in f status (args,typs,s)
+
+(*s Extraction of a constant applied to arguments. *)
+
+and extract_cst_app status context mle mlt uri ref args =
+ (* First, the [ml_schema] of the constant, in expanded version. *)
+ let status,(nb,t) = record_constant_type status ref None in
+ let status,res = expand status t in
+ let schema = nb, res in
+ (* Can we instantiate types variables for this constant ? *)
+ (* In Ocaml, inside the definition of this constant, the answer is no. *)
+ let instantiated =
+ if
+ match !current_fixpoints with None -> false | Some uri' -> NUri.eq uri uri'
+ then var2var' (snd schema)
+ else instantiation schema
+ in
+ (* Then the expected type of this constant. *)
+ let a = new_meta () in
+ (* We compare stored and expected types in two steps. *)
+ (* First, can [kn] be applied to all args ? *)
+ let metas = List.map new_meta args in
+ let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
+ (* Second, is the resulting type compatible with the expected type [mlt] ? *)
+ let magic2 = needs_magic (a, mlt) in
+ (* The internal head receives a magic if [magic1] *)
+ let head = put_magic_if magic1 (MLglob ref) in
+ (* Now, the extraction of the arguments. *)
+ let status,s_full = type2signature status (snd schema) in
+ let s_full = sign_with_implicits ref s_full in
+ let s = sign_no_final_keeps s_full in
+ let ls = List.length s in
+ let la = List.length args in
+ (* The ml arguments, already expunged from known logical ones *)
+ let status,mla = make_mlargs status context mle s args metas in
+ let mla =
+ if not magic1 then
+ try
+ let l,l' = list_chop (projection_arity status ref) mla in
+ if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
+ else mla
+ with _ -> mla
+ else mla
+ in
+ (* For strict languages, purely logical signatures with at least
+ one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
+ accordingly. *)
+ let optdummy = match sign_kind s_full with
+ | UnsafeLogicalSig -> [MLdummy]
+ | _ -> []
+ in
+ (* Different situations depending of the number of arguments: *)
+ if la >= ls
+ then
+ (* Enough args, cleanup already done in [mla], we only add the
+ additionnal dummy if needed. *)
+ status,put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
+ else
+ (* Partially applied function with some logical arg missing.
+ We complete via eta and expunge logical args. *)
+ let ls' = ls-la in
+ let s' = list_skipn la s in
+ let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
+ let e = anonym_or_dummy_lams (mlapp head mla) s' in
+ status,put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
+
+(*s Extraction of an inductive constructor applied to arguments. *)
+
+(* \begin{itemize}
+ \item In ML, contructor arguments are uncurryfied.
+ \item We managed to suppress logical parts inside inductive definitions,
+ but they must appears outside (for partial applications for instance)
+ \item We also suppressed all Coq parameters to the inductives, since
+ they are fixed, and thus are not used for the computation.
+ \end{itemize} *)
+
+and extract_cons_app status context mle mlt ref (*(((kn,i) as ip,j) as cp)*) args =
+ let uri,i,j =
+ match ref with
+ NReference.Ref (uri,NReference.Con(i,j,_)) -> uri,i,j
+ | _ -> assert false in
+ let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
+ let tyref = NReference.mk_indty b ref in
+ (* First, we build the type of the constructor, stored in small pieces. *)
+ let status,mi = extract_ind status uri in
+ let params_nb = mi.ind_nparams in
+ let oi = mi.ind_packets.(i) in
+ let nb_tvars = List.length oi.ip_vars in
+ let status,types =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = expand status x in
+ status,y::res
+ ) oi.ip_types.(j-1) (status,[]) in
+ let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
+ let type_cons = type_recomp (types, Tglob (tyref, list_tvar)) in
+ let type_cons = instantiation (nb_tvars, type_cons) in
+ (* Then, the usual variables [s], [ls], [la], ... *)
+ let status,s =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = type2sign status x in
+ status,y::res)
+ types (status,[]) in
+ let s = sign_with_implicits ref s in
+ let ls = List.length s in
+ let la = List.length args in
+ assert (la <= ls + params_nb);
+ let la' = max 0 (la - params_nb) in
+ let args' = list_lastn la' args in
+ (* Now, we build the expected type of the constructor *)
+ let metas = List.map new_meta args' in
+ (* If stored and expected types differ, then magic! *)
+ let a = new_meta () in
+ let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
+ let magic2 = needs_magic (a, mlt) in
+ let head status mla =
+ if mi.ind_kind = Singleton then
+ status, put_magic_if magic1 (List.hd mla)
+ else
+ let status,typeargs = match snd (type_decomp type_cons) with
+ | Tglob (_,l) ->
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = type_simpl status x in
+ status,y::res)
+ l (status,[])
+ | _ -> assert false
+ in
+ let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
+ status, put_magic_if magic1 (MLcons (info, ref, mla))
+ in
+ (* Different situations depending of the number of arguments: *)
+ if la < params_nb then
+ let status,head' = head status (eta_args_sign ls s) in
+ status,
+ put_magic_if magic2
+ (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
+ else
+ let status,mla = make_mlargs status context mle s args' metas in
+ if la = ls + params_nb
+ then
+ let status,res = head status mla in
+ status,put_magic_if (magic2 && not magic1) res
+ else (* [ params_nb <= la <= ls + params_nb ] *)
+ let ls' = params_nb + ls - la in
+ let s' = list_lastn ls' s in
+ let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
+ let status,res = head status mla in
+ status,put_magic_if magic2 (anonym_or_dummy_lams res s')
+
+(*S Extraction of a case. *)
+
+and extract_case context mle (ip,c,br) status mlt =
+ (* [br]: bodies of each branch (in functional form) *)
+ (* [ni]: number of arguments without parameters in each branch *)
+ let uri,i =
+ match ip with
+ NReference.Ref (uri,NReference.Ind (_,i,_)) -> uri,i
+ | _ -> assert false
+ in
+ let br_size = Array.length br in
+ if br_size = 0 then begin
+ (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
+ status,MLexn "absurd case"
+ end else
+ (* [c] has an inductive type, and is not a type scheme type. *)
+ let t = type_of status context c in
+ (* The only non-informative case: [c] is of sort [Prop] *)
+ if (sort_of status context t) = InProp then
+ begin
+ (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
+ (* Logical singleton case: *)
+ (* [match c with C i j k -> t] becomes [t'] *)
+ assert (br_size = 1);
+ let ni =
+ let _,leftno,tys,_,_ = NCicEnvironment.get_checked_indtys status ip in
+ let _,_,_,cl = List.hd tys in
+ let _,_,cty = List.hd cl in
+ let prods,_ = split_all_prods status ~subst:[] [] cty in
+ List.length prods - leftno
+ in
+ let s = iterate (fun l -> Kill Kother :: l) ni [] in
+ let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni mlt in
+ let status,e = extract_maybe_term status context mle mlt br.(0) in
+ status, snd (case_expunge s e)
+ end
+ else
+ let status,mi = extract_ind status uri in
+ let oi = mi.ind_packets.(i) in
+ let metas = Array.init (List.length oi.ip_vars) new_meta in
+ (* The extraction of the head. *)
+ let type_head = Tglob (ip, Array.to_list metas) in
+ let status,a = extract_term status context mle type_head c [] in
+ (* The extraction of each branch. *)
+ let extract_branch status i =
+ let r = NReference.mk_constructor (i+1) ip in
+ (* The types of the arguments of the corresponding constructor. *)
+ let f status t =
+ let status,res = expand status t in
+ status,type_subst_vect metas res in
+ let status,l =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = f status x in
+ status,y::res)
+ oi.ip_types.(i) (status,[]) in
+ (* the corresponding signature *)
+ let status,s =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = type2sign status x in
+ status,y::res)
+ oi.ip_types.(i) (status,[]) in
+ let s = sign_with_implicits r s in
+ (* Extraction of the branch (in functional form). *)
+ let status,e =
+ extract_maybe_term status context 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 _ -> "_") e in
+ status,(r, List.rev ids, e')
+ in
+ if mi.ind_kind = Singleton then
+ begin
+ (* Informative singleton case: *)
+ (* [match c with C i -> t] becomes [let i = c' in t'] *)
+ assert (br_size = 1);
+ let status,(_,ids,e') = extract_branch status 0 in
+ assert (List.length ids = 1);
+ status,MLletin (tmp_id (List.hd ids),a,e')
+ end
+ else
+ (* Standard case: we apply [extract_branch]. *)
+ let status,typs = List.fold_right
+ (fun x (status,res) ->
+ let status,y = type_simpl status x in
+ status,y::res)
+ (Array.to_list metas) (status,[]) in
+ let info={ m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone } in
+ let status,res =
+ array_fold_right_i
+ (fun i _ (status,res) ->
+ let status,y = extract_branch status i in
+ status,y::res) br (status,[])
+ in
+ status,MLcase (info, a, Array.of_list res)
+
+(*S ML declarations. *)
+
+(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
+ and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
+
+let rec decomp_lams_eta_n n m status context c t =
+ let rels = fst (splay_prod_n status context n t) in
+ let rels',c = decompose_lam c in
+ let d = n - m in
+ (* we'd better keep rels' as long as possible. *)
+ let rels=(list_firstn d rels)@(List.map (fun (n,t) -> n, NCic.Decl t) rels')in
+ let eta_args = List.rev_map (fun n -> NCic.Rel n) (interval 1 d) in
+ rels, NCic.Appl ((NCicSubstitution.lift status d c)::eta_args)
+
+(* Let's try to identify some situation where extracted code
+ will allow generalisation of type variables *)
+
+let rec gentypvar_ok c =
+ match c with
+ | NCic.Lambda _ -> true
+ | NCic.Const (NReference.Ref (_,
+ (NReference.Decl
+ |NReference.Def _
+ |NReference.Fix _
+ |NReference.CoFix _))) -> true
+ | NCic.Appl (c::v) ->
+ (* if all arguments are variables, these variables will
+ disappear after extraction (see [empty_s] below) *)
+ List.for_all isRel v && gentypvar_ok c
+ | _ -> false
+
+(*s From a constant to a ML declaration. *)
+
+let extract_std_constant status uri body typ =
+ reset_meta_count ();
+ (* The short type [t] (i.e. possibly with abbreviations). *)
+ let status,res = record_constant_type status uri (Some typ) in
+ let t = snd res in
+ (* The real type [t']: without head products, expanded, *)
+ (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
+ let status,res = expand status (var2var' t) in
+ let l,t' = type_decomp res in
+ let status,s =
+ List.fold_right
+ (fun x (status,res) ->
+ let status,y = type2sign status x in
+ status,y::res)
+ l (status,[]) in
+ (* Check for user-declared implicit information *)
+ let s = sign_with_implicits uri(*CSC: (ConstRef uri)*) s in
+ (* Decomposing the top level lambdas of [body].
+ If there isn't enough, it's ok, as long as remaining args
+ aren't to be pruned (and initial lambdas aren't to be all
+ removed if the target language is strict). In other situations,
+ eta-expansions create artificially enough lams (but that may
+ break user's clever let-ins and partial applications). *)
+ let rels, c =
+ let n = List.length s
+ and m = nb_lam body in
+ if n <= m then decompose_lam_n n body
+ else
+ let s,s' = list_split_at m s in
+ if List.for_all ((=) Keep) s' && sign_kind s <> UnsafeLogicalSig
+ then decompose_lam_n m body
+ else decomp_lams_eta_n n m status [] body typ
+ in
+ (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
+ let rels, c =
+ let n = List.length rels in
+ let s,s' = list_split_at n s in
+ let k = sign_kind s in
+ let empty_s = (k = EmptySig || k = SafeLogicalSig) in
+ if empty_s && not (gentypvar_ok c) && s' <> [] && type_maxvar t <> 0
+ then decomp_lams_eta_n (n+1) n status [] body typ
+ else rels,c
+ in
+ let n = List.length rels in
+ let s = list_firstn n s in
+ let l,l' = list_split_at n l in
+ let t' = type_recomp (l',t') in
+ (* The initial ML environment. *)
+ let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
+ (* The lambdas names. *)
+ let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in
+ (* The according Coq environment. *)
+ let context = rels in
+ (* The real extraction: *)
+ let status,e = extract_term status context mle t' c [] in
+ (* Expunging term and type from dummy lambdas. *)
+ let trm = term_expunge s (ids,e) in
+ let trm = handle_exn uri n (fun i -> fst (List.nth rels (i-1))) trm in
+ let status,res = type_expunge_from_sign status s t in
+ status,trm,res
+
+let extract_constant_spec status r bo typ =
+ match flag_of_type status [] typ with
+ | (Logic, TypeScheme) ->
+ status,Stype (r, [], Some (Tdummy Ktype))
+ | (Logic, Default) -> status,Sval (r, Tdummy Kother)
+ | (Info, TypeScheme) ->
+ let s,vl = type_sign_vl status [] typ in
+ (match bo with
+ | None -> status,Stype (r, vl, None)
+ | Some body ->
+ let db = db_from_sign s in
+ let status,t =
+ extract_type_scheme status [] db body (List.length s) in
+ status,Stype (r, vl, Some t))
+ | (Info, Default) ->
+ let status,(_,t) = record_constant_type status r (Some typ) in
+ let status,res = type_expunge status t in
+ status,Sval (r,res)
+
+
+let extract_fixpoint_common uri height fix_or_cofix ifl =
+ let recparamnoi,ti,ci =
+ List.fold_right
+ (fun (_,_,recparamno,ty,bo) (recparamnos,tys,bos) ->
+ recparamno::recparamnos,ty::tys,bo::bos) ifl ([],[],[]) in
+ let recparamnoi = Array.of_list recparamnoi in
+ let ti = Array.of_list ti in
+ let ci = Array.of_list ci in
+ let n = Array.length ti in
+ let vkn =
+ Array.init n
+ (fun i ->
+ if fix_or_cofix then
+ NReference.reference_of_spec uri
+ (NReference.Fix (i,recparamnoi.(i),height))
+ else
+ NReference.reference_of_spec uri (NReference.CoFix i)) in
+ ti,ci,n,vkn
+
+let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
+ let status =
+ if is_projection then
+ let _,_,recparamno,_,_ = List.nth ifl 0 in
+ let fieldspec = NReference.Fix (0,recparamno,height) in
+ let ref = NReference.reference_of_spec uri fieldspec in
+ confirm_projection status ref
+ else
+ status in
+ let ti,ci,n,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
+ let types = Array.make n (Tdummy Kother)
+ and terms = Array.make n MLdummy in
+ current_fixpoints := Some uri;
+ let status = ref status in
+ for i = 0 to n-1 do
+ if sort_of !status [] ti.(i) <> InProp then begin
+ let status',e,t = extract_std_constant !status vkn.(i) ci.(i) ti.(i) in
+ status := status';
+ terms.(i) <- e;
+ types.(i) <- t;
+ end
+ done;
+ let status = !status in
+ current_fixpoints := None;
+ status,Dfix (vkn, terms, types)
+
+let extract_fixpoint_spec status uri height fix_or_cofix ifl =
+ let ti,_,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
+ let status,specs =
+ array_mapi_status status
+ (fun status i vkn ->
+ if sort_of status [] ti.(i) <> InProp then begin
+ let status,spec = extract_constant_spec status vkn None ti.(i) in
+ status, Some spec
+ end
+ else status,None
+ ) vkn in
+ status,HExtlib.filter_map (fun x -> x) (Array.to_list specs)
+
+let extract_constant status r bo typ =
+ match bo with
+ | None -> (* A logical axiom is risky, an informative one is fatal. *)
+ (match flag_of_type status [] typ with
+ | (Info,TypeScheme) ->
+ if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
+ let n = type_scheme_nb_args status [] typ in
+ let ids = iterate (fun l -> anonymous_name::l) n [] in
+ status,Dtype (r, ids, Taxiom)
+ | (Info,Default) ->
+ if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
+ let status,(_,t) = record_constant_type status r (Some typ) in
+ let status,res = type_expunge status t in
+ status, Dterm (r, MLaxiom, res)
+ | (Logic,TypeScheme) ->
+ (*CSC: only for warnings add_log_axiom r;*)
+ status,Dtype (r, [], Tdummy Ktype)
+ | (Logic,Default) ->
+ (*CSC: only for warnings add_log_axiom r;*)
+ status,Dterm (r, MLdummy, Tdummy Kother))
+ | Some body ->
+ (match flag_of_type status [] typ with
+ | (Logic, Default) ->
+ status,Dterm (r, MLdummy, Tdummy Kother)
+ | (Logic, TypeScheme) ->
+ status,Dtype (r, [], Tdummy Ktype)
+ | (Info, Default) ->
+ let status,e,t = extract_std_constant status r body typ in
+ status,Dterm (r,e,t)
+ | (Info, TypeScheme) ->
+ let s,vl = type_sign_vl status [] typ in
+ let db = db_from_sign s in
+ let status,t =
+ extract_type_scheme status [] db body (List.length s)
+ in status,Dtype (r, vl, t))
+
+let extract_inductive status uri inductive ind_pragma leftno types =
+ let status,ind = extract_ind0 status uri inductive ind_pragma leftno types in
+ (*CSC: add_recursors status kn;*)
+ let f status _i _j l =
+ let implicits = [] (*CSC:implicits_of_global (ConstructRef ((kn,i),j+1))*) in
+ let rec filter status i = function
+ | [] -> status,[]
+ | t::l ->
+ let status,l' = filter status (succ i) l in
+ let status,res = expand status t in
+ if isDummy res || List.mem i implicits then status,l'
+ else status,t::l'
+ in filter status 1 l
+ in
+ let status,packets =
+ array_fold_right_i
+ (fun i p (status,res) ->
+ let status,types =
+ array_fold_right_i
+ (fun j x (status,res) ->
+ let status,y = f status i j x in
+ status,y::res
+ ) p.ip_types (status,[])
+ in
+ status, { p with ip_types = Array.of_list types }::res
+ ) ind.ind_packets (status,[])
+ in status,{ ind with ind_packets = Array.of_list packets }
+
+(*s Is a [ml_decl] logical ? *)
+
+let logical_decl = function
+ | Dterm (_,MLdummy,Tdummy _) -> true
+ | Dtype (_,[],Tdummy _) -> true
+ | Dfix (_,av,tv) ->
+ (array_for_all ((=) MLdummy) av) &&
+ (array_for_all isDummy tv)
+ | Dind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+ | _ -> false
+
+(*s Is a [ml_spec] logical ? *)
+
+let logical_spec = function
+ | Stype (_, [], Some (Tdummy _)) -> true
+ | Sval (_,Tdummy _) -> true
+ | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+ | _ -> false
+
+let extract_impl status (uri,height,metasenv,subst,obj_kind) =
+ assert (metasenv=[]);
+ assert (subst=[]);
+ let status,decl =
+ match obj_kind with
+ NCic.Constant (_,_,bo,typ,_) ->
+ let r =
+ let spec =
+ match bo with
+ None -> NReference.Decl
+ | Some _ -> NReference.Def height
+ in NReference.reference_of_spec uri spec
+ in
+ extract_constant status r bo typ
+ | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
+ let status,res =
+ extract_inductive status uri inductive ind_pragma leftno types
+ in
+ status,Dind res
+ | NCic.Fixpoint (fix_or_cofix,ifl,(_,_,def_pragma)) ->
+ extract_fixpoint status uri height fix_or_cofix
+ (def_pragma = `Projection) ifl
+ in
+ status, if logical_decl decl then None else Some decl
+;;
+
+let extract_spec status (uri,height,metasenv,subst,obj_kind) =
+ assert (metasenv=[]);
+ assert (subst=[]);
+ match obj_kind with
+ NCic.Constant (_,_,bo,typ,_) ->
+ let r =
+ let spec =
+ match bo with
+ None -> NReference.Decl
+ | Some _ -> NReference.Def height
+ in NReference.reference_of_spec uri spec
+ in
+ let status,spec = extract_constant_spec status r bo typ in
+ status,if logical_spec spec then [] else [spec]
+ | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
+ let status,res =
+ extract_inductive status uri inductive ind_pragma leftno types in
+ let spec = Sind res in
+ status,if logical_spec spec then [] else [spec]
+ | NCic.Fixpoint (fix_or_cofix,ifl,_) ->
+ extract_fixpoint_spec status uri height fix_or_cofix ifl
+
+let extract status obj =
+ let status,res = extract_impl status obj in
+ let status,resl = extract_spec status obj in
+ status,res,resl
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: extraction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+(*s Extraction from Coq terms to Miniml. *)
+
+open Coq
+open Miniml
+open OcamlExtractionTable
+
+val extract:
+ #OcamlExtractionTable.status as 'status -> NCic.obj ->
+ 'status * ml_decl option * ml_spec list
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+(*s Target language for extraction: a core ML called MiniML. *)
+
+open Coq
+
+(* The [signature] type is used to know how many arguments a CIC
+ 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). *)
+
+type kill_reason = Ktype | Kother
+
+type sign = Keep | Kill of kill_reason
+
+
+(* Convention: outmost lambda/product gives the head of the list. *)
+
+type signature = sign list
+
+(*s ML type expressions. *)
+
+type ml_type =
+ | Tarr of ml_type * ml_type
+ | Tglob of NReference.reference * ml_type list
+ | Tvar of int
+ | Tvar' of int (* same as Tvar, used to avoid clash *)
+ | Tmeta of ml_meta (* used during ML type reconstruction *)
+ | Tdummy of kill_reason
+ | Tunknown
+ | Taxiom
+
+and ml_meta = { id : int; mutable contents : ml_type option }
+
+(* ML type schema.
+ The integer is the number of variable in the schema. *)
+
+type ml_schema = int * ml_type
+
+(*s ML inductive types. *)
+
+type inductive_kind =
+ | Singleton
+ | Coinductive
+ | Standard
+ | Record of NReference.reference list
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
+ If the inductive is logical ([ip_logical = false]), then all other fields
+ are unused. Otherwise,
+ [ip_sign] is a signature concerning the arguments of the inductive,
+ [ip_vars] contains the names of the type variables surviving in ML,
+ [ip_types] contains the ML types of all constructors.
+*)
+
+type ml_ind_packet = {
+ ip_reference : NReference.reference;
+ ip_consreferences : NReference.reference array;
+ ip_typename : identifier;
+ ip_consnames : identifier array;
+ ip_logical : bool;
+ ip_sign : signature;
+ ip_vars : identifier list;
+ ip_types : (ml_type list) array
+}
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type ml_ind = {
+ ind_kind : inductive_kind;
+ ind_nparams : int;
+ ind_packets : ml_ind_packet array;
+}
+
+(*s ML terms. *)
+
+type ml_ident =
+ | Dummy
+ | Id of identifier
+ | Tmp of identifier
+
+(** We now store some typing information on constructors
+ and cases to avoid type-unsafe optimisations.
+ For cases, we also store the set of branches to merge
+ in a common pattern, either "_ -> c" or "x -> f x"
+*)
+
+type constructor_info = {
+ c_kind : inductive_kind;
+ c_typs : ml_type list;
+}
+
+type branch_same =
+ | BranchNone
+ | BranchFun of Intset.t
+ | BranchCst of Intset.t
+
+type match_info = {
+ m_kind : inductive_kind;
+ m_typs : ml_type list;
+ m_same : branch_same
+}
+
+type ml_branch = NReference.reference * ml_ident list * ml_ast
+
+and ml_ast =
+ | MLrel of int
+ | MLapp of ml_ast * ml_ast list
+ | MLlam of ml_ident * ml_ast
+ | MLletin of ml_ident * ml_ast * ml_ast
+ | MLglob of NReference.reference
+ | MLcons of constructor_info * NReference.reference * ml_ast list
+ | MLcase of match_info * ml_ast * ml_branch array
+ | MLfix of int * identifier array * ml_ast array
+ | MLexn of string
+ | MLdummy
+ | MLaxiom
+ | MLmagic of ml_ast
+
+(*s ML declarations. *)
+
+type ml_decl =
+ | Dind of ml_ind
+ | Dtype of NReference.reference * identifier list * ml_type
+ | Dterm of NReference.reference * ml_ast * ml_type
+ | Dfix of NReference.reference array * ml_ast array * ml_type array
+
+type ml_spec =
+ | Sind of ml_ind
+ | Stype of NReference.reference * identifier list * ml_type option
+ | Sval of NReference.reference * ml_type
+
+type ml_specif =
+ | Spec of ml_spec
+
+and ml_module_sig = (label * ml_specif) list
+
+type ml_structure_elem =
+ | SEdecl of ml_decl
+
+and ml_module_structure = (label * ml_structure_elem) list
+
+type ml_structure = module_path * ml_module_structure
+
+type ml_signature = module_path * ml_module_sig
+
+type unsafe_needs = {
+ mldummy : bool;
+ tdummy : bool;
+ tunknown : bool;
+ magic : bool
+}
+
+type language_descr = {
+ keywords : Idset.t;
+
+ (* Concerning the source file *)
+ file_suffix : string;
+ preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+ pp_struct : ml_structure -> std_ppcmds;
+
+ (* Concerning a possible interface file *)
+ sig_suffix : string option;
+ sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+ pp_sig : ml_signature -> std_ppcmds;
+
+ (* for an isolated declaration print *)
+ pp_decl : ml_decl -> std_ppcmds;
+
+}
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
+
+(*i*)
+
+open Coq
+open OcamlExtractionTable
+open Miniml
+(*i*)
+
+(*s Exceptions. *)
+
+exception Found
+exception Impossible
+
+(*S Names operations. *)
+
+let anonymous_name = "x"
+let dummy_name = "_"
+
+let anonymous = Id anonymous_name
+
+let id_of_name = function
+ | "_" -> anonymous_name
+ | id -> id
+
+let id_of_mlid = function
+ | Dummy -> dummy_name
+ | Id id -> id
+ | Tmp id -> id
+
+let tmp_id = function
+ | Id id -> Tmp id
+ | a -> a
+
+let is_tmp = function Tmp _ -> true | _ -> false
+
+(*S Operations upon ML types (with meta). *)
+
+let meta_count = ref 0
+
+let reset_meta_count () = meta_count := 0
+
+let new_meta _ =
+ incr meta_count;
+ Tmeta {id = !meta_count; contents = None}
+
+(*s Sustitution of [Tvar i] by [t] in a ML type. *)
+
+let type_subst i t0 t =
+ let rec subst t = match t with
+ | Tvar j when i = j -> t0
+ | Tmeta {contents=None} -> t
+ | Tmeta {contents=Some u} -> subst u
+ | Tarr (a,b) -> Tarr (subst a, subst b)
+ | Tglob (r, l) -> Tglob (r, List.map subst l)
+ | a -> a
+ in subst t
+
+(* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
+
+let type_subst_list l t =
+ let rec subst t = match t with
+ | Tvar j -> List.nth l (j-1)
+ | Tmeta {contents=None} -> t
+ | Tmeta {contents=Some u} -> subst u
+ | Tarr (a,b) -> Tarr (subst a, subst b)
+ | Tglob (r, l) -> Tglob (r, List.map subst l)
+ | a -> a
+ in subst t
+
+(* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *)
+
+let type_subst_vect v t =
+ let rec subst t = match t with
+ | Tvar j -> v.(j-1)
+ | Tmeta {contents=None} -> t
+ | Tmeta {contents=Some u} -> subst u
+ | Tarr (a,b) -> Tarr (subst a, subst b)
+ | Tglob (r, l) -> Tglob (r, List.map subst l)
+ | a -> a
+ in subst t
+
+(*s From a type schema to a type. All [Tvar] become fresh [Tmeta]. *)
+
+let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
+
+(*s Occur-check of a free meta in a type *)
+
+let rec type_occurs alpha t =
+ match t with
+ | Tmeta {id=beta; contents=None} -> alpha = beta
+ | Tmeta {contents=Some u} -> type_occurs alpha u
+ | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
+ | Tglob (_r,l) -> List.exists (type_occurs alpha) l
+ | _ -> false
+
+(*s Most General Unificator *)
+
+let rec mgu = function
+ | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+ | Tmeta m, t | t, Tmeta m ->
+ (match m.contents with
+ | Some u -> mgu (u, t)
+ | None when type_occurs m.id t -> raise Impossible
+ | None -> m.contents <- Some t)
+ | Tarr(a, b), Tarr(a', b') ->
+ mgu (a, a'); mgu (b, b')
+ | Tglob (r,l), Tglob (r',l') when r = r' ->
+ List.iter mgu (List.combine l l')
+ | Tdummy _, Tdummy _ -> ()
+ | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+ | _ -> raise Impossible
+
+let needs_magic p = try mgu p; false with Impossible -> true
+
+let put_magic_if b a = if b then MLmagic a else a
+
+let put_magic p a = if needs_magic p then MLmagic a else a
+
+let generalizable a =
+ match a with
+ | MLapp _ -> false
+ | _ -> true (* TODO, this is just an approximation for the moment *)
+
+(*S ML type env. *)
+
+module Mlenv = struct
+
+ let meta_cmp m m' = compare m.id m'.id
+ module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
+
+ (* Main MLenv type. [env] is the real environment, whereas [free]
+ (tries to) record the free meta variables occurring in [env]. *)
+
+ type t = { env : ml_schema list; mutable free : Metaset.t}
+
+ (* Empty environment. *)
+
+ let empty = { env = []; free = Metaset.empty }
+
+ (* [get] returns a instantiated copy of the n-th most recently added
+ type in the environment. *)
+
+ let get mle n =
+ assert (List.length mle.env >= n);
+ instantiation (List.nth mle.env (n-1))
+
+ (* [find_free] finds the free meta in a type. *)
+
+ let rec find_free set = function
+ | Tmeta m when m.contents = None -> Metaset.add m set
+ | Tmeta {contents = Some t} -> find_free set t
+ | Tarr (a,b) -> find_free (find_free set a) b
+ | Tglob (_,l) -> List.fold_left find_free set l
+ | _ -> set
+
+ (* The [free] set of an environment can be outdate after
+ some unifications. [clean_free] takes care of that. *)
+
+ let clean_free mle =
+ let rem = ref Metaset.empty
+ and add = ref Metaset.empty in
+ let clean m = match m.contents with
+ | None -> ()
+ | Some u -> rem := Metaset.add m !rem; add := find_free !add u
+ in
+ Metaset.iter clean mle.free;
+ mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add
+
+ (* From a type to a type schema. If a [Tmeta] is still uninstantiated
+ and does appears in the [mle], then it becomes a [Tvar]. *)
+
+ let generalization mle t =
+ let c = ref 0 in
+ let map = ref (Intmap.empty : int Intmap.t) in
+ let add_new i = incr c; map := Intmap.add i !c !map; !c in
+ let rec meta2var t = match t with
+ | Tmeta {contents=Some u} -> meta2var u
+ | Tmeta ({id=i} as m) ->
+ (try Tvar (Intmap.find i !map)
+ with Not_found ->
+ if Metaset.mem m mle.free then t
+ else Tvar (add_new i))
+ | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
+ | Tglob (r,l) -> Tglob (r, List.map meta2var l)
+ | t -> t
+ in !c, meta2var t
+
+ (* Adding a type in an environment, after generalizing. *)
+
+ let push_gen mle t =
+ clean_free mle;
+ { env = generalization mle t :: mle.env; free = mle.free }
+
+ (* Adding a type with no [Tvar], hence no generalization needed. *)
+
+ let push_type {env=e;free=f} t =
+ { env = (0,t) :: e; free = find_free f t}
+
+ (* Adding a type with no [Tvar] nor [Tmeta]. *)
+
+ let push_std_type {env=e;free=f} t =
+ { env = (0,t) :: e; free = f}
+
+end
+
+(*S Operations upon ML types (without meta). *)
+
+(*s Does a section path occur in a ML type ? *)
+
+let rec type_mem_kn uri =
+ function
+ | Tmeta {contents = Some t} -> type_mem_kn uri t
+ | Tglob (r,l) ->
+ let NReference.Ref (uri',_) = r in
+ NUri.eq uri uri' || List.exists (type_mem_kn uri) l
+ | Tarr (a,b) -> (type_mem_kn uri a) || (type_mem_kn uri b)
+ | _ -> false
+
+(*s Greatest variable occurring in [t]. *)
+
+let type_maxvar t =
+ let rec parse n = function
+ | Tmeta {contents = Some t} -> parse n t
+ | Tvar i -> max i n
+ | Tarr (a,b) -> parse (parse n a) b
+ | Tglob (_,l) -> List.fold_left parse n l
+ | _ -> n
+ in parse 0 t
+
+(*s What are the type variables occurring in [t]. *)
+
+let intset_union_map_list f l =
+ List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
+
+let intset_union_map_array f a =
+ Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
+
+let rec type_listvar = function
+ | Tmeta {contents = Some t} -> type_listvar t
+ | Tvar i | Tvar' i -> Intset.singleton i
+ | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
+ | Tglob (_,l) -> intset_union_map_list type_listvar l
+ | _ -> Intset.empty
+
+(*s From [a -> b -> c] to [[a;b],c]. *)
+
+let rec type_decomp = function
+ | Tmeta {contents = Some t} -> type_decomp t
+ | Tarr (a,b) -> let l,h = type_decomp b in a::l, h
+ | a -> [],a
+
+(*s The converse: From [[a;b],c] to [a -> b -> c]. *)
+
+let rec type_recomp (l,t) = match l with
+ | [] -> t
+ | a::l -> Tarr (a, type_recomp (l,t))
+
+(*s Translating [Tvar] to [Tvar'] to avoid clash. *)
+
+let rec var2var' = function
+ | Tmeta {contents = Some t} -> var2var' t
+ | Tvar i -> Tvar' i
+ | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
+ | Tglob (r,l) -> Tglob (r, List.map var2var' l)
+ | a -> a
+
+type 'status abbrev_map =
+ 'status -> NReference.reference -> ('status * ml_type) option
+
+(*s Delta-reduction of type constants everywhere in a ML type [t].
+ [env] is a function of type [ml_type_env]. *)
+
+let type_expand status env t =
+ let rec expand status = function
+ | Tmeta {contents = Some t} -> expand status t
+ | Tglob (r,l) ->
+ (match env status r with
+ | Some (status,mlt) -> expand status (type_subst_list l mlt)
+ | None ->
+ let status,l =
+ List.fold_right
+ (fun t (status,res) ->
+ let status,res' = expand status t in
+ status,res'::res)
+ l (status,[])
+ in
+ status,Tglob (r, l))
+ | Tarr (a,b) ->
+ let status,a = expand status a in
+ let status,b = expand status b in
+ status,Tarr (a,b)
+ | a -> status,a in
+ if OcamlExtractionTable.type_expand () then
+ expand status t
+ else
+ status,t
+
+let type_simpl status = type_expand status (fun _ _ -> None)
+
+(*s Generating a signature from a ML type. *)
+
+let type_to_sign status env t =
+ let status,res = type_expand status env t in
+ status,
+ match res with
+ | Tdummy d -> Kill d
+ | _ -> Keep
+
+let type_to_signature status env t =
+ let rec f = function
+ | Tmeta {contents = Some t} -> f t
+ | Tarr (Tdummy d, b) -> Kill d :: f b
+ | Tarr (_, b) -> Keep :: f b
+ | _ -> []
+ in
+ let status,res = type_expand status env t in
+ status,f res
+
+let isKill = function Kill _ -> true | _ -> false
+
+let isDummy = function Tdummy _ -> true | _ -> false
+
+let sign_of_id = function
+ | Dummy -> Kill Kother
+ | _ -> Keep
+
+(* Classification of signatures *)
+
+type sign_kind =
+ | EmptySig
+ | NonLogicalSig (* at least a [Keep] *)
+ | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
+ | SafeLogicalSig (* only [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
+
+(* 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
+ if s' = [Keep] then [] else s'
+
+(*s Removing [Tdummy] from the top level of a ML type. *)
+
+let type_expunge_from_sign status env s t =
+ let rec expunge status s t =
+ if s = [] then status,t else match t with
+ | Tmeta {contents = Some t} -> expunge status s t
+ | Tarr (a,b) ->
+ let status,t = expunge status (List.tl s) b in
+ status, if List.hd s = Keep then Tarr (a, t) else t
+ | Tglob (r,l) ->
+ (match env status r with
+ | Some (status,mlt) -> expunge status s (type_subst_list l mlt)
+ | None -> assert false)
+ | _ -> assert false
+ in
+ let status,t = expunge status (sign_no_final_keeps s) t in
+ status,
+ if sign_kind s = UnsafeLogicalSig then
+ Tarr (Tdummy Kother, t)
+ else t
+
+let type_expunge status env t =
+ let status,res = type_to_signature status env t in
+ type_expunge_from_sign status env res t
+
+(*S Generic functions over ML ast terms. *)
+
+let mlapp f a = if a = [] then f else MLapp (f,a)
+
+(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
+ of the number of bingings crossed before reaching the [MLrel]. *)
+
+let ast_iter_rel f =
+ let rec iter n = function
+ | MLrel i -> f (i-n)
+ | MLlam (_,a) -> iter (n+1) a
+ | MLletin (_,a,b) -> iter n a; iter (n+1) b
+ | MLcase (_,a,v) ->
+ iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
+ | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
+ | MLapp (a,l) -> iter n a; List.iter (iter n) l
+ | MLcons (_,_,l) -> List.iter (iter n) l
+ | MLmagic a -> iter n a
+ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
+ in iter 0
+
+(*s Map over asts. *)
+
+let ast_map_case f (c,ids,a) = (c,ids,f a)
+
+let ast_map f = function
+ | MLlam (i,a) -> MLlam (i, f a)
+ | MLletin (i,a,b) -> MLletin (i, f a, f b)
+ | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
+ | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
+ | MLapp (a,l) -> MLapp (f a, List.map f l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
+ | MLmagic a -> MLmagic (f a)
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+
+(*s Map over asts, with binding depth as parameter. *)
+
+let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
+
+let ast_map_lift f n = function
+ | MLlam (i,a) -> MLlam (i, f (n+1) a)
+ | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
+ | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
+ | MLfix (i,ids,v) ->
+ let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
+ | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
+ | MLmagic a -> MLmagic (f n a)
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
+
+(*s Iter over asts. *)
+
+let ast_iter_case f (_c,_ids,a) = f a
+
+let ast_iter f = function
+ | MLlam (_i,a) -> f a
+ | MLletin (_i,a,b) -> f a; f b
+ | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
+ | MLfix (_i,_ids,v) -> Array.iter f v
+ | MLapp (a,l) -> f a; List.iter f l
+ | MLcons (_,_c,l) -> List.iter f l
+ | MLmagic a -> f a
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
+
+(*S Operations concerning De Bruijn indices. *)
+
+(*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
+
+let ast_occurs k t =
+ try
+ ast_iter_rel (fun i -> if i = k then raise Found) t; false
+ with Found -> true
+
+(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
+ in [t] with [k<=i<=k'] *)
+
+let ast_occurs_itvl k k' t =
+ try
+ ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
+ with Found -> true
+
+(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *)
+
+let nb_occur_k k t =
+ let cpt = ref 0 in
+ ast_iter_rel (fun i -> if i = k then incr cpt) t;
+ !cpt
+
+let nb_occur t = nb_occur_k 1 t
+
+(* Number of occurences of [Rel 1] in [t], with special treatment of match:
+ occurences in different branches aren't added, but we rather use max. *)
+
+let nb_occur_match =
+ let rec nb k = function
+ | MLrel i -> if i = k then 1 else 0
+ | MLcase(_,a,v) ->
+ (nb k a) +
+ Array.fold_left
+ (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
+ | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
+ | MLfix (_,ids,v) -> let k = k+(Array.length ids) in
+ Array.fold_left (fun r a -> r+(nb k a)) 0 v
+ | MLlam (_,a) -> nb (k+1) a
+ | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
+ | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
+ | MLmagic a -> nb k a
+ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
+ in nb 1
+
+(*s Lifting on terms.
+ [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
+
+let ast_lift k t =
+ let rec liftrec n = function
+ | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
+ | a -> ast_map_lift liftrec n a
+ in if k = 0 then t else liftrec 0 t
+
+let ast_pop t = ast_lift (-1) t
+
+(*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ...
+ Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
+
+let permut_rels k k' =
+ let rec permut n = function
+ | MLrel i as a ->
+ let i' = i-n in
+ if i'<1 || i'>k+k' then a
+ else if i'<=k then MLrel (i+k')
+ else MLrel (i-k)
+ | a -> ast_map_lift permut n a
+ in permut 0
+
+(*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t].
+ Lifting (of one binder) is done at the same time. *)
+
+let ast_subst e =
+ let rec subst n = function
+ | MLrel i as a ->
+ let i' = i-n in
+ if i'=1 then ast_lift n e
+ else if i'<1 then a
+ else MLrel (i-1)
+ | a -> ast_map_lift subst n a
+ in subst 0
+
+(*s Generalized substitution.
+ [gen_subst v d t] applies to [t] the substitution coded in the
+ [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies
+ to [Rel] greater than [Array.length v]. *)
+
+let gen_subst v d t =
+ let rec subst n = function
+ | MLrel i as a ->
+ let i'= i-n in
+ if i' < 1 then a
+ else if i' <= Array.length v then
+ match v.(i'-1) with
+ | None -> MLexn ("UNBOUND " ^ string_of_int i')
+ | Some u -> ast_lift n u
+ else MLrel (i+d)
+ | a -> ast_map_lift subst n a
+ in subst 0 t
+
+(*S Operations concerning lambdas. *)
+
+(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
+ [[idn;...;id1]] and the term [t]. *)
+
+let collect_lams =
+ let rec collect acc = function
+ | MLlam(id,t) -> collect (id::acc) t
+ | x -> acc,x
+ in collect []
+
+(*s [collect_n_lams] does the same for a precise number of [MLlam]. *)
+
+let collect_n_lams =
+ let rec collect acc n t =
+ if n = 0 then acc,t
+ else match t with
+ | MLlam(id,t) -> collect (id::acc) (n-1) t
+ | _ -> assert false
+ in collect []
+
+(*s [remove_n_lams] just removes some [MLlam]. *)
+
+let rec remove_n_lams n t =
+ if n = 0 then t
+ else match t with
+ | MLlam(_,t) -> remove_n_lams (n-1) t
+ | _ -> assert false
+
+(*s [nb_lams] gives the number of head [MLlam]. *)
+
+let rec nb_lams = function
+ | MLlam(_,t) -> succ (nb_lams t)
+ | _ -> 0
+
+(*s [named_lams] does the converse of [collect_lams]. *)
+
+let rec named_lams ids a = match ids with
+ | [] -> a
+ | id :: ids -> named_lams ids (MLlam (id,a))
+
+(*s The same for a specific identifier (resp. anonymous, dummy) *)
+
+let rec many_lams id a = function
+ | 0 -> a
+ | n -> many_lams id (MLlam (id,a)) (pred n)
+
+let anonym_lams a n = many_lams anonymous a n
+let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n
+let dummy_lams a n = many_lams Dummy a n
+
+(*s mixed according to a signature. *)
+
+let rec anonym_or_dummy_lams a = function
+ | [] -> a
+ | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
+ | Kill _ :: s -> MLlam(Dummy, anonym_or_dummy_lams a s)
+
+(*S Operations concerning eta. *)
+
+(*s The following function creates [MLrel n;...;MLrel 1] *)
+
+let rec eta_args n =
+ if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+
+(*s Same, but filtered by a signature. *)
+
+let rec eta_args_sign n = function
+ | [] -> []
+ | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s)
+ | Kill _ :: s -> eta_args_sign (n-1) s
+
+(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
+
+let rec test_eta_args_lift k n = function
+ | [] -> n=0
+ | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+
+(*s Computes an eta-reduction. *)
+
+let eta_red e =
+ let ids,t = collect_lams e in
+ let n = List.length ids in
+ if n = 0 then e
+ else match t with
+ | MLapp (f,a) ->
+ let m = List.length a in
+ let ids,body,args =
+ if m = n then
+ [], f, a
+ else if m < n then
+ list_skipn m ids, f, a
+ else (* m > n *)
+ let a1,a2 = list_chop (m-n) a in
+ [], MLapp (f,a1), a2
+ in
+ let p = List.length args in
+ if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
+ then named_lams ids (ast_lift (-p) body)
+ else e
+ | _ -> e
+
+(*s Computes all head linear beta-reductions possible in [(t a)].
+ Non-linear head beta-redex become let-in. *)
+
+let rec linear_beta_red a t = match a,t with
+ | [], _ -> t
+ | a0::a, MLlam (id,t) ->
+ (match nb_occur_match t with
+ | 0 -> linear_beta_red a (ast_pop t)
+ | 1 -> linear_beta_red a (ast_subst a0 t)
+ | _ ->
+ let a = List.map (ast_lift 1) a in
+ MLletin (id, a0, linear_beta_red a t))
+ | _ -> MLapp (t, a)
+
+let rec tmp_head_lams = function
+ | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t)
+ | e -> e
+
+(*s Applies a substitution [s] of constants by their body, plus
+ linear beta reductions at modified positions.
+ Moreover, we mark some lambdas as suitable for later linear
+ reduction (this helps the inlining of recursors).
+*)
+
+let rec ast_glob_subst _s _t = assert false (*CSC: reimplement match t with
+ | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
+ let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
+ (try linear_beta_red a (Refmap'.find refe s)
+ with Not_found -> MLapp (f, a))
+ | MLglob ((ConstRef kn) as refe) ->
+ (try Refmap'.find refe s with Not_found -> t)
+ | _ -> ast_map (ast_glob_subst s) t *)
+
+
+(*S Auxiliary functions used in simplification of ML cases. *)
+
+(* Factorisation of some match branches into a common "x -> f x"
+ branch may break types sometimes. Example: [type 'x a = A].
+ Then [let id = function A -> A] has type ['x a -> 'y a],
+ which is incompatible with the type of [let id x = x].
+ We now check that the type arguments of the inductive are
+ preserved by our transformation.
+
+ TODO: this verification should be done someday modulo
+ expansion of type definitions.
+*)
+
+(*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
+ as a function [f] applied to [MLcons(r,l)]. For that it transforms
+ any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
+ if any variable in [l] occurs outside such a [MLcons] *)
+
+let branch_as_fun typs (r,l,c) =
+ let nargs = List.length l in
+ let rec genrec n = function
+ | MLrel i as c ->
+ let i' = i-n in
+ if i'<1 then c
+ else if i'>nargs then MLrel (i-nargs+1)
+ else raise Impossible
+ | MLcons(i,r',args) when
+ r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
+ MLrel (n+1)
+ | a -> ast_map_lift genrec n a
+ in genrec 0 c
+
+(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
+ independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
+ if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
+ appear like a function with one arg (for uniformity with [branch_as_fun]).
+ NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is
+ empty, i.e. when [r] is a constant constructor
+*)
+
+let branch_as_cst (_,l,c) =
+ let n = List.length l in
+ if ast_occurs_itvl 1 n c then raise Impossible;
+ ast_lift (1-n) c
+
+(* A branch [MLcons(r,l)->c] can be seen at the same time as a function
+ branch and a constant branch, either because:
+ - [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B"
+ - this constructor is constant (i.e. [l] is empty). For example "A -> A"
+ When searching for the best factorisation below, we'll try both.
+*)
+
+(* The following structure allows to record which element occurred
+ at what position, and then finally return the most frequent
+ element and its positions. *)
+
+let census_add, census_max, census_clean =
+ let h = Hashtbl.create 13 in
+ let clear () = Hashtbl.clear h in
+ let add e i =
+ let s = try Hashtbl.find h e with Not_found -> Intset.empty in
+ Hashtbl.replace h e (Intset.add i s)
+ in
+ let max e0 =
+ let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
+ Hashtbl.iter
+ (fun e s ->
+ let n = Intset.cardinal s in
+ if n > !len then begin len := n; lst := s; elm := e end)
+ h;
+ (!elm,!lst)
+ in
+ (add,max,clear)
+
+(* [factor_branches] return the longest possible list of branches
+ that have the same factorization, either as a function or as a
+ constant.
+*)
+
+let factor_branches o typs br =
+ census_clean ();
+ for i = 0 to Array.length br - 1 do
+ if o.opt_case_idr then
+ (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
+ 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
+ census_clean ();
+ let n = Intset.cardinal br_set in
+ if n = 0 then None
+ else if Array.length br >= 2 && n < 2 then None
+ else Some (br_factor, br_set)
+
+(*s If all branches are functions, try to permut the case and the functions. *)
+
+let rec merge_ids ids ids' = match ids,ids' with
+ | [],l -> l
+ | l,[] -> l
+ | i::ids, i'::ids' ->
+ (if i = Dummy then i' else i) :: (merge_ids ids ids')
+
+let is_exn = function MLexn _ -> true | _ -> false
+
+let rec permut_case_fun br _acc =
+ let nb = ref max_int in
+ Array.iter (fun (_,_,t) ->
+ let ids, c = collect_lams t in
+ let n = List.length ids in
+ if (n < !nb) && (not (is_exn c)) then nb := n) br;
+ if !nb = max_int || !nb = 0 then ([],br)
+ else begin
+ let br = Array.copy br in
+ let ids = ref [] in
+ for i = 0 to Array.length br - 1 do
+ let (r,l,t) = br.(i) in
+ let local_nb = nb_lams t in
+ if local_nb < !nb then (* t = MLexn ... *)
+ br.(i) <- (r,l,remove_n_lams local_nb t)
+ else begin
+ let local_ids,t = collect_n_lams !nb t in
+ ids := merge_ids !ids local_ids;
+ br.(i) <- (r,l,permut_rels !nb (List.length l) t)
+ end
+ done;
+ (!ids,br)
+ end
+
+(*S Generalized iota-reduction. *)
+
+(* Definition of a generalized iota-redex: it's a [MLcase(e,_)]
+ with [(is_iota_gen e)=true]. Any generalized iota-redex is
+ transformed into beta-redexes. *)
+
+let rec is_iota_gen = function
+ | MLcons _ -> true
+ | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
+ | _ -> false
+
+let constructor_index _ = assert false (*CSC: function
+ | ConstructRef (_,j) -> pred j
+ | _ -> assert false*)
+
+let iota_gen br =
+ let rec iota k = function
+ | MLcons (_i,r,a) ->
+ let (_,ids,c) = br.(constructor_index r) in
+ let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
+ let c = ast_lift k c in
+ MLapp (c,a)
+ | MLcase(i,e,br') ->
+ let new_br =
+ Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
+ in MLcase(i,e, new_br)
+ | _ -> assert false
+ in iota 0
+
+let is_atomic = function
+ | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
+ | _ -> false
+
+let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
+
+(** Program creates a let-in named "program_branch_NN" for each branch of match.
+ Unfolding them leads to more natural code (and more dummy removal) *)
+
+let is_program_branch = function
+ | Id id ->
+ let s = id in
+ let br = "program_branch_" in
+ let n = String.length br in
+ (try
+ ignore (int_of_string (String.sub s n (String.length s - n)));
+ String.sub s 0 n = br
+ with _ -> false)
+ | Tmp _ | Dummy -> false
+
+let expand_linear_let o id e =
+ o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
+
+(*S The main simplification function. *)
+
+(* Some beta-iota reductions + simplifications. *)
+
+let rec simpl o = function
+ | MLapp (f, []) -> simpl o f
+ | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
+ | MLcase (i,e,br) ->
+ let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
+ simpl_case o i br (simpl o e)
+ | MLletin(Dummy,_,e) -> simpl o (ast_pop e)
+ | MLletin(id,c,e) ->
+ let e = simpl o e in
+ if
+ (is_atomic c) || (is_atomic e) ||
+ (let n = nb_occur_match e in
+ (n = 0 || (n=1 && expand_linear_let o id e)))
+ then
+ simpl o (ast_subst c e)
+ else
+ MLletin(id, simpl o c, e)
+ | MLfix(i,ids,c) ->
+ let n = Array.length ids in
+ if ast_occurs_itvl 1 n c.(i) then
+ MLfix (i, ids, Array.map (simpl o) c)
+ else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
+ | a -> ast_map (simpl o) a
+
+(* invariant : list [a] of arguments is non-empty *)
+
+and simpl_app o a = function
+ | MLapp (f',a') -> simpl_app o (a'@a) f'
+ | MLlam (Dummy,t) ->
+ simpl o (MLapp (ast_pop t, List.tl a))
+ | MLlam (id,t) -> (* Beta redex *)
+ (match nb_occur_match t with
+ | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
+ | 1 when (is_tmp id || o.opt_lin_beta) ->
+ simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
+ | _ ->
+ let a' = List.map (ast_lift 1) (List.tl a) in
+ simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
+ | MLletin (id,e1,e2) when o.opt_let_app ->
+ (* Application of a letin: we push arguments inside *)
+ MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
+ | MLcase (i,e,br) when o.opt_case_app ->
+ (* Application of a case: we push arguments inside *)
+ let br' =
+ Array.map
+ (fun (n,l,t) ->
+ let k = List.length l in
+ let a' = List.map (ast_lift k) a in
+ (n, l, simpl o (MLapp (t,a')))) br
+ in simpl o (MLcase (i,e,br'))
+ | (MLdummy | MLexn _) as e -> e
+ (* We just discard arguments in those cases. *)
+ | f -> MLapp (f,a)
+
+(* Invariant : all empty matches should now be [MLexn] *)
+
+and simpl_case o i br e =
+ if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
+ simpl o (iota_gen br e)
+ else
+ (* Swap the case and the lam if possible *)
+ let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
+ let n = List.length ids in
+ if n <> 0 then
+ simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
+ else
+ (* Can we merge several branches as the same constant or function ? *)
+ match factor_branches o i.m_typs br with
+ | Some (f,ints) when Intset.cardinal ints = Array.length br ->
+ (* If all branches have been factorized, we remove the match *)
+ simpl o (MLletin (Tmp anonymous_name, e, f))
+ | Some (f,ints) ->
+ let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
+ in MLcase ({i with m_same=same}, e, br)
+ | None -> MLcase (i, e, br)
+
+(*S Local prop elimination. *)
+(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
+
+(*s In a list, it selects only the elements corresponding to a [Keep]
+ in the boolean list [l]. *)
+
+let rec select_via_bl l args = match l,args with
+ | [],_ -> args
+ | Keep::l,a::args -> a :: (select_via_bl l args)
+ | Kill _::l,_a::args -> select_via_bl l args
+ | _ -> assert false
+
+(*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
+ the other [Rels] are made correct via a [gen_subst].
+ Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
+
+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 n = n' then ids,c
+ else if n' = 0 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 _ :: l -> parse_ids (i+1) j l
+ in parse_ids 0 1 bl;
+ select_via_bl bl ids, gen_subst v (n'-n) c
+ end
+
+(*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding
+ to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or
+ if there is no lambda left at all. *)
+
+let kill_dummy_lams c =
+ let ids,c = collect_lams c in
+ let bl = List.map sign_of_id ids in
+ if not (List.mem Keep bl) then raise Impossible;
+ let rec fst_kill n = function
+ | [] -> raise Impossible
+ | Kill _ :: _bl -> n
+ | Keep :: bl -> fst_kill (n+1) bl
+ in
+ let skip = max 0 ((fst_kill 0 bl) - 1) in
+ let ids_skip, ids = list_chop skip ids in
+ let _, bl = list_chop skip bl in
+ let c = named_lams ids_skip c in
+ let ids',c = kill_some_lams bl (ids,c) in
+ ids, named_lams ids' c
+
+(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
+ and a signature [s] and builds a eta-long version. *)
+
+(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is :
+ [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)] with [c' = lift 4 c] *)
+
+let eta_expansion_sign s (ids,c) =
+ let rec abs ids rels i = function
+ | [] ->
+ 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
+ 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]. *)
+
+let case_expunge s e =
+ let m = List.length s in
+ let n = nb_lams e in
+ let p = if m <= n then collect_n_lams m e
+ else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+ kill_some_lams (List.rev s) p
+
+(*s [term_expunge] takes a function [fun idn ... id1 -> c]
+ and a signature [s] and remove dummy lams. The difference
+ with [case_expunge] is that we here leave one dummy lambda
+ if all lambdas are logical dummy and the target language is strict. *)
+
+let term_expunge s (ids,c) =
+ if s = [] then c
+ else
+ let ids,c = kill_some_lams (List.rev s) (ids,c) in
+ if ids = [] && List.mem (Kill Kother) s then
+ MLlam (Dummy, ast_lift 1 c)
+ else named_lams ids c
+
+(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+ purge the args of [MLrel r] corresponding to a [dummy_name].
+ It makes eta-expansion if needed. *)
+
+let kill_dummy_args ids r t =
+ let m = List.length ids in
+ let bl = List.rev_map sign_of_id ids in
+ let rec found n = function
+ | MLrel r' when r' = r + n -> true
+ | MLmagic e -> found n e
+ | _ -> false
+ in
+ let rec killrec n = function
+ | MLapp(e, a) when found n e ->
+ let k = max 0 (m - (List.length a)) in
+ let a = List.map (killrec n) a in
+ let a = List.map (ast_lift k) a in
+ let a = select_via_bl bl (a @ (eta_args k)) in
+ named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+ | e when found n e ->
+ let a = select_via_bl bl (eta_args m) in
+ named_lams ids (MLapp (ast_lift m e, a))
+ | e -> ast_map_lift killrec n e
+ in killrec 0 t
+
+(*s The main function for local [dummy] elimination. *)
+
+let rec kill_dummy = function
+ | MLfix(i,fi,c) ->
+ (try
+ let ids,c = kill_dummy_fix i c in
+ ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
+ with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
+ | MLapp (MLfix (i,fi,c),a) ->
+ let a = List.map kill_dummy a in
+ (try
+ let ids,c = kill_dummy_fix i c in
+ let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
+ let fake' = kill_dummy_args ids 1 fake in
+ ast_subst (MLfix (i,fi,c)) fake'
+ with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
+ | MLletin(id, MLfix (i,fi,c),e) ->
+ (try
+ let ids,c = kill_dummy_fix i c in
+ let e = kill_dummy (kill_dummy_args ids 1 e) in
+ MLletin(id, MLfix(i,fi,c),e)
+ with Impossible ->
+ MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
+ | MLletin(id,c,e) ->
+ (try
+ let ids,c = kill_dummy_lams (kill_dummy_hd c) in
+ let e = kill_dummy (kill_dummy_args ids 1 e) in
+ let c = kill_dummy c in
+ if is_atomic c then ast_subst c e else MLletin (id, c, e)
+ with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
+ | a -> ast_map kill_dummy a
+
+(* Similar function, but acting only on head lambdas and let-ins *)
+
+and kill_dummy_hd = function
+ | MLlam(id,e) -> MLlam(id, kill_dummy_hd e)
+ | MLletin(id,c,e) ->
+ (try
+ let ids,c = kill_dummy_lams (kill_dummy_hd c) in
+ let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
+ let c = kill_dummy c in
+ if is_atomic c then ast_subst c e else MLletin (id, c, e)
+ with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
+ | a -> a
+
+and kill_dummy_fix i c =
+ let n = Array.length c in
+ let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
+ let c = Array.copy c in c.(i) <- ci;
+ for j = 0 to (n-1) do
+ c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
+ done;
+ ids,c
+
+(*s Putting things together. *)
+
+let normalize a =
+ let o = optims () in
+ let rec norm a =
+ let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
+ if a = a' then a else norm a'
+ in norm a
+
+(*S Special treatment of fixpoint for pretty-printing purpose. *)
+
+let general_optimize_fix f ids n args m c =
+ let v = Array.make n 0 in
+ for i=0 to (n-1) do v.(i)<-i done;
+ let aux i = function
+ | MLrel j when v.(j-1)>=0 ->
+ if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
+ | _ -> raise Impossible
+ in list_iter_i aux args;
+ let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
+ let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
+ let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
+ MLfix(0,[|f|],[|new_c|])
+
+let optimize_fix a =
+ if not (optims()).opt_fix_fun then a
+ else
+ let ids,a' = collect_lams a in
+ let n = List.length ids in
+ if n = 0 then a
+ else match a' with
+ | MLfix(_,[|f|],[|c|]) ->
+ let new_f = MLapp (MLrel (n+1),eta_args n) in
+ let new_c = named_lams ids (normalize (ast_subst new_f c))
+ in MLfix(0,[|f|],[|new_c|])
+ | MLapp(a',args) ->
+ let m = List.length args in
+ (match a' with
+ | MLfix(_,_,_) when
+ (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a')
+ -> a'
+ | MLfix(_,[|f|],[|c|]) ->
+ (try general_optimize_fix f ids n args m c
+ with Impossible -> a)
+ | _ -> a)
+ | _ -> a
+
+(*S Inlining. *)
+
+(* Utility functions used in the decision of inlining. *)
+
+let rec ml_size = function
+ | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
+ | MLlam(_,t) -> 1 + ml_size t
+ | MLcons(_,_,l) -> ml_size_list l
+ | MLcase(_,t,pv) ->
+ 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
+ | MLfix(_,_,f) -> ml_size_array f
+ | MLletin (_,_,t) -> ml_size t
+ | MLmagic t -> ml_size t
+ | _ -> 0
+
+and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
+
+and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
+
+let is_fix = function MLfix _ -> true | _ -> false
+
+let rec is_constr = function
+ | MLcons _ -> true
+ | MLlam(_,t) -> is_constr t
+ | _ -> false
+
+(*s Strictness *)
+
+(* A variable is strict if the evaluation of the whole term implies
+ the evaluation of this variable. Non-strict variables can be found
+ behind Match, for example. Expanding a term [t] is a good idea when
+ it begins by at least one non-strict lambda, since the corresponding
+ argument to [t] might be unevaluated in the expanded code. *)
+
+exception Toplevel
+
+let lift n l = List.map ((+) n) l
+
+let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l
+
+(* This function returns a list of de Bruijn indices of non-strict variables,
+ or raises [Toplevel] if it has an internal non-strict variable.
+ In fact, not all variables are checked for strictness, only the ones which
+ de Bruijn index is in the candidates list [cand]. The flag [add] controls
+ the behaviour when going through a lambda: should we add the corresponding
+ variable to the candidates? We use this flag to check only the external
+ lambdas, those that will correspond to arguments. *)
+
+let rec non_stricts add cand = function
+ | MLlam (_id,t) ->
+ let cand = lift 1 cand in
+ let cand = if add then 1::cand else cand in
+ pop 1 (non_stricts add cand t)
+ | MLrel n ->
+ List.filter ((<>) n) cand
+ | MLapp (t,l)->
+ let cand = non_stricts false cand t in
+ List.fold_left (non_stricts false) cand l
+ | MLcons (_,_,l) ->
+ List.fold_left (non_stricts false) cand l
+ | MLletin (_,t1,t2) ->
+ let cand = non_stricts false cand t1 in
+ pop 1 (non_stricts add (lift 1 cand) t2)
+ | MLfix (_,i,f)->
+ let n = Array.length i in
+ let cand = lift n cand in
+ let cand = Array.fold_left (non_stricts false) cand f in
+ pop n cand
+ | MLcase (_,t,v) ->
+ (* The only interesting case: for a variable to be non-strict, *)
+ (* it is sufficient that it appears non-strict in at least one branch, *)
+ (* so we make an union (in fact a merge). *)
+ let cand = non_stricts false cand t in
+ Array.fold_left
+ (fun c (_,i,t)->
+ let n = List.length i in
+ let cand = lift n cand in
+ let cand = pop n (non_stricts add cand t) in
+ Sort.merge (<=) cand c) [] v
+ (* [merge] may duplicates some indices, but I don't mind. *)
+ | MLmagic t ->
+ non_stricts add cand t
+ | _ ->
+ cand
+
+(* The real test: we are looking for internal non-strict variables, so we start
+ with no candidates, and the only positive answer is via the [Toplevel]
+ exception. *)
+
+let is_not_strict t =
+ try let _ = non_stricts true [] t in false
+ with Toplevel -> true
+
+(*s Inlining decision *)
+
+(* [inline_test] answers the following question:
+ If we could inline [t] (the user said nothing special),
+ should we inline ?
+
+ We expand small terms with at least one non-strict
+ variable (i.e. a variable that may not be evaluated).
+
+ Futhermore we don't expand fixpoints.
+
+ Moreover, as mentionned by X. Leroy (bug #2241),
+ inling a constant from inside an opaque module might
+ break types. To avoid that, we require below that
+ both [r] and its body are globally visible. This isn't
+ fully satisfactory, since [r] might not be visible (functor),
+ and anyway it might be interesting to inline [r] at least
+ inside its own structure. But to be safe, we adopt this
+ restriction for the moment.
+*)
+
+let inline_test _r _t =
+ (*CSC:if not (auto_inline ()) then*) false
+(*
+ else
+ let c = match r with ConstRef c -> c | _ -> assert false in
+ let body = try (Global.lookup_constant c).const_body with _ -> None in
+ if body = None then false
+ else
+ let t1 = eta_red t in
+ let t2 = snd (collect_lams t1) in
+ not (is_fix t2) && ml_size t < 12 && is_not_strict t
+*)
+
+(*CSC: (not) reimplemented
+let con_of_string s =
+ let null = empty_dirpath in
+ match repr_dirpath (dirpath_of_string s) with
+ | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
+ | [] -> assert false
+
+let manual_inline_set =
+ List.fold_right (fun x -> Cset_env.add (con_of_string x))
+ [ "Coq.Init.Wf.well_founded_induction_type";
+ "Coq.Init.Wf.well_founded_induction";
+ "Coq.Init.Wf.Acc_iter";
+ "Coq.Init.Wf.Fix_F";
+ "Coq.Init.Wf.Fix";
+ "Coq.Init.Datatypes.andb";
+ "Coq.Init.Datatypes.orb";
+ "Coq.Init.Logic.eq_rec_r";
+ "Coq.Init.Logic.eq_rect_r";
+ "Coq.Init.Specif.proj1_sig";
+ ]
+ Cset_env.empty*)
+
+let manual_inline = function (*CSC:
+ | ConstRef c -> Cset_env.mem c manual_inline_set
+ |*) _ -> false
+
+(* If the user doesn't say he wants to keep [t], we inline in two cases:
+ \begin{itemize}
+ \item the user explicitly requests it
+ \item [expansion_test] answers that the inlining is a good idea, and
+ we are free to act (AutoInline is set)
+ \end{itemize} *)
+
+let inline _r _t = false (*CSC: we never inline atm
+ (*CSC:not (to_keep r) (* The user DOES want to keep it *)
+ && not (is_inline_custom r)
+ &&*) (false(*to_inline r*) (* The user DOES want to inline it *)
+ || (not (is_projection r) &&
+ (is_recursor r || manual_inline r || inline_test r t)))
+*)
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
+
+open OcamlExtractionTable
+open Miniml
+open Coq
+
+(*s Utility functions over ML types with meta. *)
+
+val reset_meta_count : unit -> unit
+val new_meta : 'a -> ml_type
+
+val type_subst : int -> ml_type -> ml_type -> ml_type
+val type_subst_list : ml_type list -> ml_type -> ml_type
+val type_subst_vect : ml_type array -> ml_type -> ml_type
+
+val instantiation : ml_schema -> ml_type
+
+val needs_magic : ml_type * ml_type -> bool
+val put_magic_if : bool -> ml_ast -> ml_ast
+val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
+
+val generalizable : ml_ast -> bool
+
+(*s ML type environment. *)
+
+module Mlenv : sig
+ type t
+ val empty : t
+
+ (* get the n-th more recently entered schema and instantiate it. *)
+ val get : t -> int -> ml_type
+
+ (* Adding a type in an environment, after generalizing free meta *)
+ val push_gen : t -> ml_type -> t
+
+ (* Adding a type with no [Tvar] *)
+ val push_type : t -> ml_type -> t
+
+ (* Adding a type with no [Tvar] nor [Tmeta] *)
+ val push_std_type : t -> ml_type -> t
+end
+
+(*s Utility functions over ML types without meta *)
+
+val type_mem_kn : NUri.uri -> ml_type -> bool
+
+val type_maxvar : ml_type -> int
+
+val type_decomp : ml_type -> ml_type list * ml_type
+val type_recomp : ml_type list * ml_type -> ml_type
+
+val var2var' : ml_type -> ml_type
+
+type 'status abbrev_map =
+ 'status -> NReference.reference -> ('status * ml_type) option
+
+val type_expand :
+ #status as 'status -> 'status abbrev_map -> ml_type -> 'status * ml_type
+val type_simpl : #status as 'status -> ml_type -> 'status * ml_type
+val type_to_sign :
+ #status as 'status -> 'status abbrev_map -> ml_type -> 'status * sign
+val type_to_signature :
+ #status as 'status -> 'status abbrev_map -> ml_type -> 'status * signature
+val type_expunge :
+ #status as 'status -> 'status abbrev_map -> ml_type -> 'status * ml_type
+val type_expunge_from_sign :
+ #status as 'status -> 'status abbrev_map -> signature -> ml_type -> 'status * ml_type
+
+val isDummy : ml_type -> bool
+val isKill : sign -> bool
+
+val case_expunge : signature -> ml_ast -> ml_ident list * ml_ast
+val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
+
+
+(*s Special identifiers. [dummy_name] is to be used for dead code
+ and will be printed as [_] in concrete (Caml) code. *)
+
+val anonymous_name : identifier
+val dummy_name : identifier
+val id_of_name : string -> identifier
+val id_of_mlid : ml_ident -> identifier
+val tmp_id : ml_ident -> ml_ident
+
+(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
+ the list [idn;...;id1] and the term [t]. *)
+
+val collect_lams : ml_ast -> ml_ident list * ml_ast
+val collect_n_lams : int -> ml_ast -> ml_ident list * ml_ast
+val remove_n_lams : int -> ml_ast -> ml_ast
+val nb_lams : ml_ast -> int
+val named_lams : ml_ident list -> ml_ast -> ml_ast
+val dummy_lams : ml_ast -> int -> ml_ast
+val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast
+
+val eta_args_sign : int -> signature -> ml_ast list
+
+(*s Utility functions over ML terms. *)
+
+val mlapp : ml_ast -> ml_ast list -> ml_ast
+val ast_map : (ml_ast -> ml_ast) -> ml_ast -> ml_ast
+val ast_map_lift : (int -> ml_ast -> ml_ast) -> int -> ml_ast -> ml_ast
+val ast_iter : (ml_ast -> unit) -> ml_ast -> unit
+val ast_occurs : int -> ml_ast -> bool
+val ast_occurs_itvl : int -> int -> ml_ast -> bool
+val ast_lift : int -> ml_ast -> ml_ast
+val ast_pop : ml_ast -> ml_ast
+val ast_subst : ml_ast -> ml_ast -> ml_ast
+
+val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast
+
+val normalize : ml_ast -> ml_ast
+val optimize_fix : ml_ast -> ml_ast
+val inline : NReference.reference -> ml_ast -> bool
+
+exception Impossible
+val branch_as_fun : ml_type list -> ml_branch -> ml_ast
+val branch_as_cst : ml_branch -> ml_ast
+
+(* Classification of signatures *)
+
+type sign_kind =
+ | EmptySig
+ | NonLogicalSig (* at least a [Keep] *)
+ | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
+ | SafeLogicalSig (* only [Kill Ktype] *)
+
+val sign_kind : signature -> sign_kind
+
+val sign_no_final_keeps : signature -> signature
--- /dev/null
+(* Copyright (C) 2000, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* $Id: cicPp.ml 7413 2007-05-29 15:30:53Z tassi $ *)
+
+let fix_sorts t = t;;
+let apply_subst subst t = assert (subst=[]); t;;
+
+type typformerreference = NReference.reference
+type reference = NReference.reference
+
+type kind =
+ | Type
+ | KArrow of kind * kind
+ | KSkip of kind (* dropped abstraction *)
+
+let rec size_of_kind =
+ function
+ | Type -> 1
+ | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r
+ | KSkip k -> size_of_kind k
+;;
+
+let bracket ?(prec=1) size_of pp o =
+ if size_of o > prec then
+ "(" ^ pp o ^ ")"
+ else
+ pp o
+;;
+
+let rec pretty_print_kind =
+ function
+ | Type -> "*"
+ | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r
+ | KSkip k -> pretty_print_kind k
+;;
+
+type typ =
+ | Var of int
+ | Unit
+ | Top
+ | TConst of typformerreference
+ | Arrow of typ * typ
+ | TSkip of typ
+ | Forall of string * kind * typ
+ | TAppl of typ list
+
+let rec size_of_type =
+ function
+ | Var _ -> 0
+ | Unit -> 0
+ | Top -> 0
+ | TConst _ -> 0
+ | Arrow _ -> 2
+ | TSkip t -> size_of_type t
+ | Forall _ -> 2
+ | TAppl _ -> 1
+;;
+
+(* None = dropped abstraction *)
+type typ_context = (string * kind) option list
+type term_context = (string * [`OfKind of kind | `OfType of typ]) option list
+
+type typ_former_decl = typ_context * kind
+type typ_former_def = typ_former_decl * typ
+
+type term =
+ | Rel of int
+ | UnitTerm
+ | Const of reference
+ | Lambda of string * (* typ **) term
+ | Appl of term list
+ | LetIn of string * (* typ **) term * term
+ | Match of reference * term * (term_context * term) list
+ | BottomElim
+ | TLambda of string * term
+ | Inst of (*typ_former **) term
+ | Skip of term
+ | UnsafeCoerce of term
+;;
+
+type term_former_decl = term_context * typ
+type term_former_def = term_former_decl * term
+
+let mk_appl f x =
+ match f with
+ Appl args -> Appl (args@[x])
+ | _ -> Appl [f;x]
+
+let mk_tappl f l =
+ match f with
+ TAppl args -> TAppl (args@l)
+ | _ -> TAppl (f::l)
+
+let rec size_of_term =
+ function
+ | Rel _ -> 1
+ | UnitTerm -> 1
+ | Const _ -> 1
+ | Lambda (_, body) -> 1 + size_of_term body
+ | Appl l -> List.length l
+ | LetIn (_, def, body) -> 1 + size_of_term def + size_of_term body
+ | Match (_, case, pats) -> 1 + size_of_term case + List.length pats
+ | BottomElim -> 1
+ | TLambda (_,t) -> size_of_term t
+ | Inst t -> size_of_term t
+ | Skip t -> size_of_term t
+ | UnsafeCoerce t -> 1 + size_of_term t
+;;
+
+module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
+
+module GlobalNames = Set.Make(String)
+
+type info_el =
+ string * [`Type of typ_context * typ option | `Constructor of typ | `Function of typ ]
+type info = (NReference.reference * info_el) list
+type db = info_el ReferenceMap.t * GlobalNames.t
+
+let empty_info = []
+
+type obj_kind =
+ TypeDeclaration of typ_former_decl
+ | TypeDefinition of typ_former_def
+ | TermDeclaration of term_former_decl
+ | TermDefinition of term_former_def
+ | LetRec of (info * NReference.reference * obj_kind) list
+ (* reference, left, right, constructors *)
+ | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list
+
+type obj = info * NReference.reference * obj_kind
+
+(* For LetRec and Algebraic blocks *)
+let dummyref =
+ NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)"
+
+type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
+
+let max_not_term t1 t2 =
+ match t1,t2 with
+ `KindOrType,_
+ | _,`KindOrType -> `KindOrType
+ | `Kind,_
+ | _,`Kind -> `Kind
+ | `Type,_
+ | _,`Type -> `Type
+ | `PropKind,_
+ | _,`PropKind -> `PropKind
+ | `Proposition,`Proposition -> `Proposition
+
+let sup = List.fold_left max_not_term `Proposition
+
+let rec classify_not_term status context t =
+ match NCicReduction.whd status ~subst:[] context t with
+ | NCic.Sort s ->
+ (match s with
+ NCic.Prop
+ | NCic.Type [`CProp,_] -> `PropKind
+ | NCic.Type [`Type,_] -> `Kind
+ | NCic.Type _ -> assert false)
+ | NCic.Prod (b,s,t) ->
+ (*CSC: using invariant on "_" *)
+ classify_not_term status ((b,NCic.Decl s)::context) t
+ | NCic.Implicit _
+ | NCic.LetIn _
+ | NCic.Const (NReference.Ref (_,NReference.CoFix _))
+ | NCic.Appl [] ->
+ assert false (* NOT POSSIBLE *)
+ | NCic.Lambda (n,s,t) ->
+ (* Lambdas can me met in branches of matches, expecially when the
+ output type is a product *)
+ classify_not_term status ((n,NCic.Decl s)::context) t
+ | NCic.Match (_,_,_,pl) ->
+ let classified_pl = List.map (classify_not_term status context) pl in
+ sup classified_pl
+ | NCic.Const (NReference.Ref (_,NReference.Fix _)) ->
+ assert false (* IMPOSSIBLE *)
+ | NCic.Meta _ -> assert false (* TODO *)
+ | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)->
+ let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in
+ let _,_,_,_,bo = List.nth l i in
+ classify_not_term status [] bo
+ | NCic.Appl (he::_) -> classify_not_term status context he
+ | NCic.Rel n ->
+ let rec find_sort typ =
+ match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with
+ NCic.Sort NCic.Prop -> `Proposition
+ | NCic.Sort (NCic.Type [`CProp,_]) -> `Proposition
+ | NCic.Sort (NCic.Type [`Type,_]) ->
+ (*CSC: we could be more precise distinguishing the user provided
+ minimal elements of the hierarchies and classify these
+ as `Kind *)
+ `KindOrType
+ | NCic.Sort (NCic.Type _) -> assert false (* ALGEBRAIC *)
+ | NCic.Prod (_,_,t) ->
+ (* we skipped arguments of applications, so here we need to skip
+ products *)
+ find_sort t
+ | _ -> assert false (* NOT A SORT *)
+ in
+ (match List.nth context (n-1) with
+ _,NCic.Decl typ -> find_sort typ
+ | _,NCic.Def _ -> assert false (* IMPOSSIBLE *))
+ | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) ->
+ let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in
+ (match classify_not_term status [] ty with
+ | `Proposition
+ | `Type -> assert false (* IMPOSSIBLE *)
+ | `Kind
+ | `KindOrType -> `Type
+ | `PropKind -> `Proposition)
+ | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
+ let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
+ let _,_,arity,_ = List.nth ityl i in
+ (match classify_not_term status [] arity with
+ | `Proposition
+ | `Type
+ | `KindOrType -> assert false (* IMPOSSIBLE *)
+ | `Kind -> `Type
+ | `PropKind -> `Proposition)
+ | NCic.Const (NReference.Ref (_,NReference.Con _))
+ | NCic.Const (NReference.Ref (_,NReference.Def _)) ->
+ assert false (* IMPOSSIBLE *)
+;;
+
+let classify status ~metasenv context t =
+ match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with
+ | NCic.Sort _ ->
+ (classify_not_term status context t : not_term :> [> not_term])
+ | ty ->
+ let ty = fix_sorts ty in
+ `Term
+ (match classify_not_term status context ty with
+ | `Proposition -> `Proof
+ | `Type -> `Term
+ | `KindOrType -> `TypeFormerOrTerm
+ | `Kind -> `TypeFormer
+ | `PropKind -> `PropFormer)
+;;
+
+
+let rec kind_of status ~metasenv context k =
+ match NCicReduction.whd status ~subst:[] context k with
+ | NCic.Sort NCic.Type _ -> Type
+ | NCic.Sort _ -> assert false (* NOT A KIND *)
+ | NCic.Prod (b,s,t) ->
+ (match classify status ~metasenv context s with
+ | `Kind ->
+ KArrow (kind_of status ~metasenv context s,
+ kind_of ~metasenv status ((b,NCic.Decl s)::context) t)
+ | `Type
+ | `KindOrType
+ | `Proposition
+ | `PropKind ->
+ KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t)
+ | `Term _ -> assert false (* IMPOSSIBLE *))
+ | NCic.Implicit _
+ | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
+ | NCic.Lambda _
+ | NCic.Rel _
+ | NCic.Const _ -> assert false (* NOT A KIND *)
+ | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
+ otherwise NOT A KIND *)
+ | NCic.Meta _
+ | NCic.Match (_,_,_,_) -> assert false (* TODO *)
+;;
+
+let rec skip_args status ~metasenv context =
+ function
+ | _,[] -> []
+ | [],_ -> assert false (* IMPOSSIBLE *)
+ | None::tl1,_::tl2 -> skip_args status ~metasenv context (tl1,tl2)
+ | _::tl1,arg::tl2 ->
+ match classify status ~metasenv context arg with
+ | `KindOrType
+ | `Type
+ | `Term `TypeFormer ->
+ Some arg::skip_args status ~metasenv context (tl1,tl2)
+ | `Kind
+ | `Proposition
+ | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
+ | `Term _ -> assert false (* IMPOSSIBLE *)
+;;
+
+class type g_status =
+ object
+ method extraction_db: db
+ end
+
+class virtual status =
+ object
+ inherit NCic.status
+ val extraction_db = ReferenceMap.empty, GlobalNames.empty
+ method extraction_db = extraction_db
+ method set_extraction_db v = {< extraction_db = v >}
+ method set_extraction_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< extraction_db = o#extraction_db >}
+ end
+
+let xdo_pretty_print_type = ref (fun _ _ -> assert false)
+let do_pretty_print_type status ctx t =
+ !xdo_pretty_print_type (status : #status :> status) ctx t
+
+let xdo_pretty_print_term = ref (fun _ _ -> assert false)
+let do_pretty_print_term status ctx t =
+ !xdo_pretty_print_term (status : #status :> status) ctx t
+
+let term_ctx_of_type_ctx =
+ List.map
+ (function
+ None -> None
+ | Some (name,k) -> Some (name,`OfKind k))
+
+let rec split_kind_prods context =
+ function
+ | KArrow (so,ta)-> split_kind_prods (Some ("_",so)::context) ta
+ | KSkip ta -> split_kind_prods (None::context) ta
+ | Type -> context,Type
+;;
+
+let rec split_typ_prods context =
+ function
+ | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta
+ | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta
+ | TSkip ta -> split_typ_prods (None::context) ta
+ | _ as t -> context,t
+;;
+
+let rec glue_ctx_typ ctx typ =
+ match ctx with
+ | [] -> typ
+ | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ))
+ | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ))
+ | None::ctx -> glue_ctx_typ ctx (TSkip typ)
+;;
+
+let rec split_typ_lambdas status n ~metasenv context typ =
+ if n = 0 then context,typ
+ else
+ match NCicReduction.whd status ~delta:max_int ~subst:[] context typ with
+ | NCic.Lambda (name,s,t) ->
+ split_typ_lambdas status (n-1) ~metasenv ((name,NCic.Decl s)::context) t
+ | t ->
+ (* eta-expansion required *)
+ let ty = NCicTypeChecker.typeof status ~metasenv ~subst:[] context t in
+ match NCicReduction.whd status ~delta:max_int ~subst:[] context ty with
+ | NCic.Prod (name,typ,_) ->
+ split_typ_lambdas status (n-1) ~metasenv
+ ((name,NCic.Decl typ)::context)
+ (NCicUntrusted.mk_appl t [NCic.Rel 1])
+ | _ -> assert false (* IMPOSSIBLE *)
+;;
+
+
+let rev_context_of_typformer status ~metasenv context =
+ function
+ NCic.Const (NReference.Ref (_,NReference.Ind _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
+ (try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Type (ctx,_) -> List.rev ctx
+ | `Constructor _
+ | `Function _ -> assert false
+ with
+ Not_found ->
+ (* This can happen only when we are processing the type of
+ the constructor of a small singleton type. In this case
+ we are not interested in all the type, but only in its
+ backbone. That is why we can safely return the dummy context
+ here *)
+ let rec dummy = None::dummy in
+ dummy)
+ | NCic.Match _ -> assert false (* TODO ???? *)
+ | NCic.Rel n ->
+ let typ =
+ match List.nth context (n-1) with
+ _,NCic.Decl typ -> typ
+ | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in
+ let typ_ctx = snd (HExtlib.split_nth n context) in
+ let typ = kind_of status ~metasenv typ_ctx typ in
+ List.rev (fst (split_kind_prods [] typ))
+ | NCic.Meta _ -> assert false (* TODO *)
+ | NCic.Const (NReference.Ref (_,NReference.Con _))
+ | NCic.Const (NReference.Ref (_,NReference.CoFix _))
+ | NCic.Sort _ | NCic.Implicit _ | NCic.Lambda _ | NCic.LetIn _
+ | NCic.Appl _ | NCic.Prod _ ->
+ assert false (* IMPOSSIBLE *)
+
+let rec typ_of status ~metasenv context k =
+ match NCicReduction.whd status ~delta:max_int ~subst:[] context k with
+ | NCic.Prod (b,s,t) ->
+ (* CSC: non-invariant assumed here about "_" *)
+ (match classify status ~metasenv context s with
+ | `Kind ->
+ Forall (b, kind_of status ~metasenv context s,
+ typ_of ~metasenv status ((b,NCic.Decl s)::context) t)
+ | `Type
+ | `KindOrType -> (* ??? *)
+ Arrow (typ_of status ~metasenv context s,
+ typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
+ | `PropKind
+ | `Proposition ->
+ TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t)
+ | `Term _ -> assert false (* IMPOSSIBLE *))
+ | NCic.Sort _
+ | NCic.Implicit _
+ | NCic.LetIn _ -> assert false (* IMPOSSIBLE *)
+ | NCic.Lambda _ -> Top (*assert false (* LAMBDA-LIFT INNER DECLARATION *)*)
+ | NCic.Rel n -> Var n
+ | NCic.Const ref -> TConst ref
+ | NCic.Match (_,_,_,_)
+ | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) ->
+ Top
+ | NCic.Appl (he::args) ->
+ let rev_he_context= rev_context_of_typformer status ~metasenv context he in
+ TAppl (typ_of status ~metasenv context he ::
+ List.map
+ (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
+ (skip_args status ~metasenv context (rev_he_context,args)))
+ | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
+ otherwise NOT A TYPE *)
+ | NCic.Meta _ -> assert false (*TODO*)
+;;
+
+let rec fomega_lift_type_from n k =
+ function
+ | Var m as t -> if m < k then t else Var (m + n)
+ | Top -> Top
+ | TConst _ as t -> t
+ | Unit -> Unit
+ | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2)
+ | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t)
+ | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t)
+ | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args)
+
+let fomega_lift_type n t =
+ if n = 0 then t else fomega_lift_type_from n 0 t
+
+let fomega_lift_term n t =
+ let rec fomega_lift_term n k =
+ function
+ | Rel m as t -> if m < k then t else Rel (m + n)
+ | BottomElim
+ | UnitTerm
+ | Const _ as t -> t
+ | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t)
+ | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t)
+ | Appl args -> Appl (List.map (fomega_lift_term n k) args)
+ | LetIn (name,m,bo) ->
+ LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo)
+ | Match (ref,t,pl) ->
+ let lift_p (ctx,t) =
+ let lift_context ctx =
+ let len = List.length ctx in
+ HExtlib.list_mapi
+ (fun el i ->
+ let j = len - i - 1 in
+ match el with
+ None
+ | Some (_,`OfKind _) as el -> el
+ | Some (name,`OfType t) ->
+ Some (name,`OfType (fomega_lift_type_from n (k+j) t))
+ ) ctx
+ in
+ lift_context ctx, fomega_lift_term n (k + List.length ctx) t
+ in
+ Match (ref,fomega_lift_term n k t,List.map lift_p pl)
+ | Inst t -> Inst (fomega_lift_term n k t)
+ | Skip t -> Skip (fomega_lift_term n (k+1) t)
+ | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t)
+ in
+ if n = 0 then t else fomega_lift_term n 0 t
+;;
+
+let rec fomega_subst k t1 =
+ function
+ | Var n ->
+ if k=n then fomega_lift_type (k-1) t1
+ else if n < k then Var n
+ else Var (n-1)
+ | Top -> Top
+ | TConst ref -> TConst ref
+ | Unit -> Unit
+ | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2)
+ | TSkip t -> TSkip (fomega_subst (k+1) t1 t)
+ | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
+ | TAppl (he::args) ->
+ mk_tappl (fomega_subst k t1 he) (List.map (fomega_subst k t1) args)
+ | TAppl [] -> assert false
+
+let fomega_lookup status ref =
+ try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Type (_,bo) -> bo
+ | `Constructor _
+ | `Function _ -> assert false
+ with
+ Not_found ->
+prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); None
+
+let rec fomega_whd status ty =
+ match ty with
+ | TConst r ->
+ (match fomega_lookup status r with
+ None -> ty
+ | Some ty -> fomega_whd status ty)
+ | TAppl (TConst r::args) ->
+ (match fomega_lookup status r with
+ None -> ty
+ | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty))
+ | _ -> ty
+
+let rec fomega_conv_kind k1 k2 =
+ match k1,k2 with
+ Type,Type -> true
+ | KArrow (s1,t1), KArrow (s2,t2) ->
+ fomega_conv_kind s1 s2 && fomega_conv_kind t1 t2
+ | KSkip k1, KSkip k2 -> fomega_conv_kind k1 k2
+ | _,_ -> false
+
+let rec fomega_conv status t1 t2 =
+ match fomega_whd status t1, fomega_whd status t2 with
+ Var n, Var m -> n=m
+ | Unit, Unit -> true
+ | Top, Top -> true
+ | TConst r1, TConst r2 -> NReference.eq r1 r2
+ | Arrow (s1,t1), Arrow (s2,t2) ->
+ fomega_conv status s1 s2 && fomega_conv status t1 t2
+ | TSkip t1, TSkip t2 -> fomega_conv status t1 t2
+ | Forall (_,k1,t1), Forall (_,k2,t2) ->
+ fomega_conv_kind k1 k2 && fomega_conv status t1 t2
+ | TAppl tl1, TAppl tl2 ->
+ (try
+ List.fold_left2 (fun b t1 t2 -> b && fomega_conv status t1 t2)
+ true tl1 tl2
+ with
+ Invalid_argument _ -> false)
+ | _,_ -> false
+
+exception PatchMe (* BUG: constructor of singleton type :-( *)
+
+let type_of_constructor status ref =
+ try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Constructor ty -> ty
+ | _ -> assert false
+ with
+ Not_found -> raise PatchMe (* BUG: constructor of singleton type :-( *)
+
+let type_of_appl_he status ~metasenv context =
+ function
+ NCic.Const (NReference.Ref (_,NReference.Con _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Def _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Decl) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref)
+ | NCic.Const (NReference.Ref (_,NReference.CoFix _) as ref) ->
+ (try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Type _ -> assert false
+ | `Constructor ty
+ | `Function ty -> ty
+ with
+ Not_found -> assert false)
+ | NCic.Const (NReference.Ref (_,NReference.Ind _)) ->
+ assert false (* IMPOSSIBLE *)
+ | NCic.Rel n ->
+ (match List.nth context (n-1) with
+ _,NCic.Decl typ
+ | _,NCic.Def (_,typ) ->
+ (* recomputed every time *)
+ typ_of status ~metasenv context
+ (NCicSubstitution.lift status n typ))
+ | (NCic.Lambda _
+ | NCic.LetIn _
+ | NCic.Match _) as t ->
+ (* BUG: here we should implement a real type-checker since we are
+ trusting the translation of the Cic one that could be wrong
+ (e.g. pruned abstractions, etc.) *)
+ (typ_of status ~metasenv context
+ (NCicTypeChecker.typeof status ~metasenv ~subst:[] context t))
+ | NCic.Meta _ -> assert false (* TODO *)
+ | NCic.Sort _ | NCic.Implicit _ | NCic.Appl _ | NCic.Prod _ ->
+ assert false (* IMPOSSIBLE *)
+
+let rec term_of status ~metasenv context =
+ function
+ | NCic.Implicit _
+ | NCic.Sort _
+ | NCic.Prod _ -> assert false (* IMPOSSIBLE *)
+ | NCic.Lambda (b,ty,bo) ->
+ (* CSC: non-invariant assumed here about "_" *)
+ (match classify status ~metasenv context ty with
+ | `Kind ->
+ TLambda (b,term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
+ | `KindOrType (* ??? *)
+ | `Type ->
+ Lambda (b, term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
+ | `PropKind
+ | `Proposition ->
+ (* CSC: LAZY ??? *)
+ Skip (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo)
+ | `Term _ -> assert false (* IMPOSSIBLE *))
+ | NCic.LetIn (b,ty,t,bo) ->
+ (match classify status ~metasenv context t with
+ | `Term `TypeFormerOrTerm (* ???? *)
+ | `Term `Term ->
+ LetIn (b,term_of status ~metasenv context t,
+ term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo)
+ | `Kind
+ | `Type
+ | `KindOrType
+ | `PropKind
+ | `Proposition
+ | `Term `PropFormer
+ | `Term `TypeFormer
+ | `Term `Proof ->
+ (* not in programming languages, we expand it *)
+ term_of status ~metasenv context
+ (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo))
+ | NCic.Rel n -> Rel n
+ | NCic.Const ref -> Const ref
+ | NCic.Appl (he::args) ->
+ let hety = type_of_appl_he status ~metasenv context he in
+ eat_args status metasenv (term_of status ~metasenv context he) context
+ hety args
+ | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
+ otherwise NOT A TYPE *)
+ | NCic.Meta _ -> assert false (* TODO *)
+ | NCic.Match (ref,_,t,pl) ->
+ let patterns_of pl =
+ let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
+ let rec eat_branch n ty context ctx pat =
+ match (ty, pat) with
+ | TSkip t,_
+ | Forall (_,_,t),_
+ | Arrow (_, t), _ when n > 0 ->
+ eat_branch (pred n) t context ctx pat
+ | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*)
+ (*CSC: unify the three cases below? *)
+ | Arrow (_, t), NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Forall (_,_,t),NCic.Lambda (name, ty, t') ->
+ let ctx =
+ (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | TSkip t,NCic.Lambda (name, ty, t') ->
+ let ctx = None::ctx in
+ let context = (name,NCic.Decl ty)::context in
+ eat_branch 0 t context ctx t'
+ | Top,_ -> assert false (* IMPOSSIBLE *)
+ | TSkip _, _
+ | Forall _,_
+ | Arrow _,_ -> assert false (*BUG here, eta-expand!*)
+ | _, _ -> context,ctx, pat
+ in
+ try
+ HExtlib.list_mapi
+ (fun pat i ->
+ let ref = NReference.mk_constructor (i+1) ref in
+ let ty =
+ (* BUG HERE, QUICK BUG WRONG PATCH IN PLACE *)
+ try
+ type_of_constructor status ref
+ with
+ PatchMe ->
+ typ_of status ~metasenv context
+ (NCicTypeChecker.typeof status ~metasenv ~subst:[] context
+ (NCic.Const ref))
+ in
+ let context,lhs,rhs = eat_branch leftno ty context [] pat in
+ let rhs =
+ (* UnsafeCoerce not always required *)
+ UnsafeCoerce (term_of status ~metasenv context rhs)
+ in
+ lhs,rhs
+ ) pl
+ with Invalid_argument _ -> assert false
+ in
+ (match classify_not_term status [] (NCic.Const ref) with
+ | `PropKind
+ | `KindOrType
+ | `Kind -> assert false (* IMPOSSIBLE *)
+ | `Proposition ->
+ (match patterns_of pl with
+ [] -> BottomElim
+ | [lhs,rhs] -> fomega_lift_term (- List.length lhs) rhs
+ | _ -> assert false)
+ | `Type ->
+ Match (ref,term_of status ~metasenv context t, patterns_of pl))
+and eat_args status metasenv acc context tyhe =
+ function
+ [] -> acc
+ | arg::tl ->
+ match fomega_whd status tyhe with
+ Arrow (s,t) ->
+ let acc =
+ match s with
+ Unit -> mk_appl acc UnitTerm
+ | _ ->
+ let foarg = term_of status ~metasenv context arg in
+ (* BUG HERE, we should implement a real type-checker instead of
+ trusting the Cic type *)
+ let inferredty =
+ typ_of status ~metasenv context
+ (NCicTypeChecker.typeof status ~metasenv ~subst:[] context arg)in
+ if fomega_conv status inferredty s then
+ mk_appl acc foarg
+ else
+(
+prerr_endline ("ARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg);
+let context = List.map fst context in
+prerr_endline ("HE = " ^ do_pretty_print_term status context acc);
+prerr_endline ("CONTEXT= " ^ String.concat " " context);
+prerr_endline ("NOT CONV: " ^ do_pretty_print_type status context inferredty ^ " vs " ^ do_pretty_print_type status context s);
+ mk_appl acc (UnsafeCoerce foarg)
+)
+ in
+ eat_args status metasenv acc context (fomega_subst 1 Unit t) tl
+ | Top ->
+ let arg =
+ match classify status ~metasenv context arg with
+ | `PropKind
+ | `Proposition
+ | `Term `TypeFormer
+ | `Term `PropFormer
+ | `Term `Proof
+ | `Type
+ | `KindOrType
+ | `Kind -> UnitTerm
+ | `Term `TypeFormerOrTerm
+ | `Term `Term -> term_of status ~metasenv context arg
+ in
+ (* BUG: what if an argument of Top has been erased??? *)
+ eat_args status metasenv
+ (UnsafeCoerce (mk_appl acc (UnsafeCoerce arg)))
+ context Top tl
+ | Forall (_,_,t) ->
+(*
+prerr_endline "FORALL";
+let xcontext = List.map fst context in
+prerr_endline ("TYPE: " ^ do_pretty_print_type status xcontext (fomega_whd status tyhe));
+prerr_endline ("fARG = " ^ status#ppterm ~metasenv ~subst:[] ~context arg);
+prerr_endline ("fHE = " ^ do_pretty_print_term status xcontext acc);
+prerr_endline ("fCONTEXT= " ^ String.concat " " xcontext);
+*)
+ (match classify status ~metasenv context arg with
+ | `PropKind -> assert false (*TODO: same as below, coercion needed???*)
+ | `Proposition
+ | `Kind ->
+ eat_args status metasenv (UnsafeCoerce (Inst acc))
+ context (fomega_subst 1 Unit t) tl
+ | `KindOrType
+ | `Term `TypeFormer
+ | `Type ->
+ eat_args status metasenv (Inst acc)
+ context (fomega_subst 1 (typ_of status ~metasenv context arg) t)
+ tl
+ | `Term _ -> assert false (*TODO: ????*))
+ | TSkip t ->
+ eat_args status metasenv acc context t tl
+ | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
+;;
+
+type 'a result =
+ | Erased
+ | OutsideTheory
+ | Failure of string
+ | Success of 'a
+;;
+
+let fresh_name_of_ref status ref =
+ (*CSC: Patch while we wait for separate compilation *)
+ let candidate =
+ let name = NCicPp.r2s status true ref in
+ let NReference.Ref (uri,_) = ref in
+ let path = NUri.baseuri_of_uri uri in
+ let path = String.sub path 5 (String.length path - 5) in
+ let path = Str.global_replace (Str.regexp "/") "_" path in
+ path ^ "_" ^ name
+ in
+ let rec freshen candidate =
+ if GlobalNames.mem candidate (snd status#extraction_db) then
+ freshen (candidate ^ "'")
+ else
+ candidate
+ in
+ freshen candidate
+
+let register_info (db,names) (ref,(name,_ as info_el)) =
+ ReferenceMap.add ref info_el db,GlobalNames.add name names
+
+let register_name_and_info status (ref,info_el) =
+ let name = fresh_name_of_ref status ref in
+ let info = ref,(name,info_el) in
+ let infos,names = status#extraction_db in
+ status#set_extraction_db (register_info (infos,names) info), info
+
+let register_infos = List.fold_left register_info
+
+let object_of_constant status ~metasenv ref bo ty =
+ match classify status ~metasenv [] ty with
+ | `Kind ->
+ let ty = kind_of status ~metasenv [] ty in
+ let ctx0,res = split_kind_prods [] ty in
+ let ctx,bo =
+ split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in
+ (match classify status ~metasenv ctx bo with
+ | `Type
+ | `KindOrType -> (* ?? no kind formers in System F_omega *)
+ let nicectx =
+ List.map2
+ (fun p1 n ->
+ HExtlib.map_option (fun (_,k) ->
+ (*CSC: BUG here, clashes*)
+ String.uncapitalize (fst n),k) p1)
+ ctx0 ctx
+ in
+ let bo = typ_of status ~metasenv ctx bo in
+ let info = ref,`Type (nicectx,Some bo) in
+ let status,info = register_name_and_info status info in
+ status,Success ([info],ref,TypeDefinition((nicectx,res),bo))
+ | `Kind -> status, Erased (* DPM: but not really, more a failure! *)
+ | `PropKind
+ | `Proposition -> status, Erased
+ | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.")
+ | `PropKind
+ | `Proposition -> status, Erased
+ | `KindOrType (* ??? *)
+ | `Type ->
+ let ty = typ_of status ~metasenv [] ty in
+ let info = ref,`Function ty in
+ let status,info = register_name_and_info status info in
+ status,
+ Success ([info],ref, TermDefinition (split_typ_prods [] ty,
+ term_of status ~metasenv [] bo))
+ | `Term _ -> status, Failure "Non-term classified as a term. This is a bug."
+;;
+
+let object_of_inductive status ~metasenv uri ind leftno il =
+ let status,_,rev_tyl =
+ List.fold_left
+ (fun (status,i,res) (_,_,arity,cl) ->
+ match classify_not_term status [] arity with
+ | `Proposition
+ | `KindOrType
+ | `Type -> assert false (* IMPOSSIBLE *)
+ | `PropKind -> status,i+1,res
+ | `Kind ->
+ let arity = kind_of status ~metasenv [] arity in
+ let ctx,_ = split_kind_prods [] arity in
+ let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in
+ let ref =
+ NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in
+ let info = ref,`Type (ctx,None) in
+ let status,info = register_name_and_info status info in
+ let _,status,cl_rev,infos =
+ List.fold_left
+ (fun (j,status,res,infos) (_,_,ty) ->
+ let ctx,ty =
+ NCicReduction.split_prods status ~subst:[] [] leftno ty in
+ let ty = typ_of status ~metasenv ctx ty in
+ let left = term_ctx_of_type_ctx left in
+ let full_ty = glue_ctx_typ left ty in
+ let ref = NReference.mk_constructor j ref in
+ let info = ref,`Constructor full_ty in
+ let status,info = register_name_and_info status info in
+ j+1,status,((ref,ty)::res),info::infos
+ ) (1,status,[],[]) cl
+ in
+ status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
+ ) (status,0,[]) il
+ in
+ match rev_tyl with
+ [] -> status,Erased
+ | _ -> status, Success ([], dummyref, Algebraic (List.rev rev_tyl))
+;;
+
+let object_of status (uri,height,metasenv,subst,obj_kind) =
+ let obj_kind = apply_subst subst obj_kind in
+ match obj_kind with
+ | NCic.Constant (_,_,None,ty,_) ->
+ let ref = NReference.reference_of_spec uri NReference.Decl in
+ (match classify status ~metasenv [] ty with
+ | `Kind ->
+ let ty = kind_of status ~metasenv [] ty in
+ let ctx,_ as res = split_kind_prods [] ty in
+ let info = ref,`Type (ctx,None) in
+ let status,info = register_name_and_info status info in
+ status, Success ([info],ref, TypeDeclaration res)
+ | `PropKind
+ | `Proposition -> status, Erased
+ | `Type
+ | `KindOrType (*???*) ->
+ let ty = typ_of status ~metasenv [] ty in
+ let info = ref,`Function ty in
+ let status,info = register_name_and_info status info in
+ status,Success ([info],ref,
+ TermDeclaration (split_typ_prods [] ty))
+ | `Term _ -> status, Failure "Type classified as a term. This is a bug.")
+ | NCic.Constant (_,_,Some bo,ty,_) ->
+ let ref = NReference.reference_of_spec uri (NReference.Def height) in
+ object_of_constant status ~metasenv ref bo ty
+ | NCic.Fixpoint (fix_or_cofix,fs,_) ->
+ let _,status,objs =
+ List.fold_right
+ (fun (_,_name,recno,ty,bo) (i,status,res) ->
+ let ref =
+ if fix_or_cofix then
+ NReference.reference_of_spec
+ uri (NReference.Fix (i,recno,height))
+ else
+ NReference.reference_of_spec uri (NReference.CoFix i)
+ in
+ let status,obj = object_of_constant ~metasenv status ref bo ty in
+ match obj with
+ | Success (info,ref,obj) -> i+1,status, (info,ref,obj)::res
+ | _ -> i+1,status, res) fs (0,status,[])
+ in
+ status, Success ([],dummyref,LetRec objs)
+ | NCic.Inductive (ind,leftno,il,_) ->
+ object_of_inductive status ~metasenv uri ind leftno il
+
+(************************ HASKELL *************************)
+
+(* -----------------------------------------------------------------------------
+ * Helper functions I can't seem to find anywhere in the OCaml stdlib?
+ * -----------------------------------------------------------------------------
+ *)
+let (|>) f g =
+ fun x -> g (f x)
+;;
+
+let curry f x y =
+ f (x, y)
+;;
+
+let uncurry f (x, y) =
+ f x y
+;;
+
+let rec char_list_of_string s =
+ let l = String.length s in
+ let rec aux buffer s =
+ function
+ | 0 -> buffer
+ | m -> aux (s.[m - 1]::buffer) s (m - 1)
+ in
+ aux [] s l
+;;
+
+let string_of_char_list s =
+ let rec aux buffer =
+ function
+ | [] -> buffer
+ | x::xs -> aux (String.make 1 x ^ buffer) xs
+ in
+ aux "" s
+;;
+
+(* ----------------------------------------------------------------------------
+ * Haskell name management: prettyfying valid and idiomatic Haskell identifiers
+ * and type variable names.
+ * ----------------------------------------------------------------------------
+ *)
+
+let remove_underscores_and_mark l =
+ let rec aux char_list_buffer positions_buffer position =
+ function
+ | [] -> (string_of_char_list char_list_buffer, positions_buffer)
+ | x::xs ->
+ if x == '_' then
+ aux char_list_buffer (position::positions_buffer) position xs
+ else
+ aux (x::char_list_buffer) positions_buffer (position + 1) xs
+ in
+ if l = ['_'] then "_",[] else aux [] [] 0 l
+;;
+
+let rec capitalize_marked_positions s =
+ function
+ | [] -> s
+ | x::xs ->
+ if x < String.length s then
+ let c = Char.uppercase (String.get s x) in
+ let _ = String.set s x c in
+ capitalize_marked_positions s xs
+ else
+ capitalize_marked_positions s xs
+;;
+
+let contract_underscores_and_capitalise =
+ char_list_of_string |>
+ remove_underscores_and_mark |>
+ uncurry capitalize_marked_positions
+;;
+
+let idiomatic_haskell_type_name_of_string =
+ contract_underscores_and_capitalise |>
+ String.capitalize
+;;
+
+let idiomatic_haskell_term_name_of_string =
+ contract_underscores_and_capitalise |>
+ String.uncapitalize
+;;
+
+let classify_reference status ref =
+ try
+ match snd (ReferenceMap.find ref (fst status#extraction_db)) with
+ `Type _ -> `TypeName
+ | `Constructor _ -> `Constructor
+ | `Function _ -> `FunctionName
+ with
+ Not_found ->
+prerr_endline ("BUG, THIS SHOULD NEVER HAPPEN " ^ NReference.string_of_reference ref); `FunctionName
+;;
+
+let capitalize classification name =
+ match classification with
+ | `Constructor
+ | `TypeName -> idiomatic_haskell_type_name_of_string name
+ | `TypeVariable
+ | `BoundVariable
+ | `FunctionName -> idiomatic_haskell_term_name_of_string name
+;;
+
+let pp_ref status ref =
+ capitalize (classify_reference status ref)
+ (try fst (ReferenceMap.find ref (fst status#extraction_db))
+ with Not_found ->
+prerr_endline ("BUG with coercions: " ^ NReference.string_of_reference ref);
+(*assert false*)
+ NCicPp.r2s status true ref (* BUG: this should never happen *)
+)
+
+(* cons avoid duplicates *)
+let rec (@:::) name l =
+ if name <> "" (* propositional things *) && name.[0] = '_' then
+ let name = String.sub name 1 (String.length name - 1) in
+ let name = if name = "" then "a" else name in
+ name @::: l
+ else if List.mem name l then (name ^ "'") @::: l
+ else name,l
+;;
+
+let (@::) x l = let x,l = x @::: l in x::l;;
+
+let rec pretty_print_type status ctxt =
+ function
+ | Var n -> List.nth ctxt (n-1)
+ | Unit -> "()"
+ | Top -> "GHC.Prim.Any"
+ | TConst ref -> pp_ref status ref
+ | Arrow (t1,t2) ->
+ bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
+ pretty_print_type status ("_"::ctxt) t2
+ | TSkip t -> pretty_print_type status ("_"::ctxt) t
+ | Forall (name, kind, t) ->
+ (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
+ let name = capitalize `TypeVariable name in
+ let name,ctxt = name@:::ctxt in
+ if size_of_kind kind > 1 then
+ "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t
+ else
+ "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t
+ | TAppl tl ->
+ String.concat " "
+ (List.map
+ (fun t -> bracket ~prec:0 size_of_type
+ (pretty_print_type status ctxt) t) tl)
+;;
+
+xdo_pretty_print_type := pretty_print_type;;
+
+
+let pretty_print_term_context status ctx1 ctx2 =
+ let name_context, rev_res =
+ List.fold_right
+ (fun el (ctx1,rev_res) ->
+ match el with
+ None -> ""@::ctx1,rev_res
+ | Some (name,`OfKind _) ->
+ let name = capitalize `TypeVariable name in
+ name@::ctx1,rev_res
+ | Some (name,`OfType typ) ->
+ let name = capitalize `TypeVariable name in
+ let name,ctx1 = name@:::ctx1 in
+ name::ctx1,
+ ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res
+ ) ctx2 (ctx1,[]) in
+ name_context, String.concat " " (List.rev rev_res)
+
+let rec pretty_print_term status ctxt =
+ function
+ | Rel n -> List.nth ctxt (n-1)
+ | UnitTerm -> "()"
+ | Const ref -> pp_ref status ref
+ | Lambda (name,t) ->
+ let name = capitalize `BoundVariable name in
+ let name,ctxt = name@:::ctxt in
+ "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t
+ | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl)
+ | LetIn (name,s,t) ->
+ let name = capitalize `BoundVariable name in
+ let name,ctxt = name@:::ctxt in
+ "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^
+ pretty_print_term status (name::ctxt) t
+ | BottomElim ->
+ "error \"Unreachable code\""
+ | UnsafeCoerce t ->
+ "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t
+ | Match (r,matched,pl) ->
+ if pl = [] then
+ "error \"Case analysis over empty type\""
+ else
+ "case " ^ pretty_print_term status ctxt matched ^ " of {\n" ^
+ String.concat " ;\n"
+ (HExtlib.list_mapi
+ (fun (bound_names,rhs) i ->
+ let ref = NReference.mk_constructor (i+1) r in
+ let name = pp_ref status ref in
+ let ctxt,bound_names =
+ pretty_print_term_context status ctxt bound_names in
+ let body =
+ pretty_print_term status ctxt rhs
+ in
+ " " ^ name ^ " " ^ bound_names ^ " -> " ^ body
+ ) pl) ^ "}\n "
+ | Skip t -> pretty_print_term status ("[[skipped]]"@::ctxt) t
+ | TLambda (name,t) ->
+ let name = capitalize `TypeVariable name in
+ pretty_print_term status (name@::ctxt) t
+ | Inst t -> pretty_print_term status ctxt t
+;;
+
+xdo_pretty_print_term := pretty_print_term;;
+
+let rec pp_obj status (_,ref,obj_kind) =
+ let pretty_print_context ctx =
+ String.concat " " (List.rev (snd
+ (List.fold_right
+ (fun (x,kind) (l,res) ->
+ let x,l = x @:::l in
+ if size_of_kind kind > 1 then
+ x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res
+ else
+ x::l,x::res)
+ (HExtlib.filter_map (fun x -> x) ctx) ([],[]))))
+ in
+ let namectx_of_ctx ctx =
+ List.fold_right (@::)
+ (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
+ match obj_kind with
+ TypeDeclaration (ctx,_) ->
+ (* data?? unsure semantics: inductive type without constructor, but
+ not matchable apparently *)
+ if List.length ctx = 0 then
+ "data " ^ pp_ref status ref
+ else
+ "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx
+ | TypeDefinition ((ctx, _),ty) ->
+ let namectx = namectx_of_ctx ctx in
+ if List.length ctx = 0 then
+ "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty
+ else
+ "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty
+ | TermDeclaration (ctx,ty) ->
+ let name = pp_ref status ref in
+ name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^
+ name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\""
+ | TermDefinition ((ctx,ty),bo) ->
+ let name = pp_ref status ref in
+ let namectx = namectx_of_ctx ctx in
+ (*CSC: BUG here *)
+ name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^
+ name ^ " = " ^ pretty_print_term status namectx bo
+ | LetRec l ->
+ String.concat "\n" (List.map (pp_obj status) l)
+ | Algebraic il ->
+ String.concat "\n"
+ (List.map
+ (fun _,ref,left,right,cl ->
+ "data " ^ pp_ref status ref ^ " " ^
+ pretty_print_context (right@left) ^ " where\n " ^
+ String.concat "\n " (List.map
+ (fun ref,tys ->
+ let namectx = namectx_of_ctx left in
+ pp_ref status ref ^ " :: " ^
+ pretty_print_type status namectx tys
+ ) cl) (*^ "\n deriving (Prelude.Show)"*)
+ ) il)
+ (* inductive and records missing *)
+
+let rec infos_of (info,_,obj_kind) =
+ info @
+ match obj_kind with
+ LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l)
+ | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l)
+ | _ -> []
+
+let haskell_of_obj status (uri,_,_,_,_ as obj) =
+ let status, obj = object_of status obj in
+ status,
+ match obj with
+ Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[]
+ | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[]
+ | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[]
+ | Success o -> pp_obj status o ^ "\n", infos_of o
+
+let refresh_uri_in_typ ~refresh_uri_in_reference =
+ let rec refresh_uri_in_typ =
+ function
+ | Var _
+ | Unit
+ | Top as t -> t
+ | TConst r -> TConst (refresh_uri_in_reference r)
+ | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2)
+ | TSkip t -> TSkip (refresh_uri_in_typ t)
+ | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t)
+ | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl)
+ in
+ refresh_uri_in_typ
+
+let refresh_uri_in_info ~refresh_uri_in_reference infos =
+ List.map
+ (function (ref,el) ->
+ match el with
+ name,`Constructor typ ->
+ let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
+ refresh_uri_in_reference ref, (name,`Constructor typ)
+ | name,`Function typ ->
+ let typ = refresh_uri_in_typ ~refresh_uri_in_reference typ in
+ refresh_uri_in_reference ref, (name,`Function typ)
+ | name,`Type (ctx,typ) ->
+ let typ =
+ match typ with
+ None -> None
+ | Some t -> Some (refresh_uri_in_typ ~refresh_uri_in_reference t)
+ in
+ refresh_uri_in_reference ref, (name,`Type (ctx,typ)))
+ infos
--- /dev/null
+(*
+ ||M|| This file is part of HELM, an Hypertextual, Electronic
+ ||A|| Library of Mathematics, developed at the Computer Science
+ ||T|| Department, University of Bologna, Italy.
+ ||I||
+ ||T|| HELM is free software; you can redistribute it and/or
+ ||A|| modify it under the terms of the GNU General Public License
+ \ / version 2 or (at your option) any later version.
+ \ / This software is distributed as is, NO WARRANTY.
+ V_______________________________________________________________ *)
+
+(* $Id: nCicEnvironment.mli 11172 2011-01-11 21:06:37Z sacerdot $ *)
+
+type info
+type db
+
+class type g_status =
+ object
+ method extraction_db: db
+ end
+
+class virtual status :
+ object ('self)
+ inherit g_status
+ inherit NCic.status
+ method set_extraction_db: db -> 'self
+ method set_extraction_status: #g_status -> 'self
+ end
+
+val empty_info: info
+
+val refresh_uri_in_info:
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+ info -> info
+
+val register_infos: db -> info -> db
+
+(* Haskell *)
+val haskell_of_obj: (#status as 'status) -> NCic.obj ->
+ 'status * (string * info)
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+(*s Production of Ocaml syntax. *)
+
+open OcamlExtractionTable
+open Coq
+open Miniml
+open Mlutil
+open Common
+
+
+(*s Some utility functions. *)
+
+let pp_tvar id =
+ let s = id in
+ if String.length s < 2 || s.[1]<>'\''
+ then str ("'"^s)
+ else str ("' "^s)
+
+let pp_tuple_light status f = function
+ | [] -> status,mt ()
+ | [x] -> f status true x
+ | l ->
+ let status,res =
+ prlist_with_sep_status status
+ (fun () -> str "," ++ spc ()) (fun status -> f status false) l in
+ status, pp_par true res
+
+let pp_tuple status f = function
+ | [] -> status,mt ()
+ | [x] -> f status x
+ | l ->
+ let status,res =
+ prlist_with_sep_status status (fun () -> str "," ++ spc ()) f l in
+ status,pp_par true res
+
+let pp_boxed_tuple f = function
+ | [] -> mt ()
+ | [x] -> f x
+ | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
+
+let pp_abst = function
+ | [] -> mt ()
+ | l ->
+ str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
+ str " ->" ++ spc ()
+
+let pp_parameters l =
+ (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+
+(*s Ocaml renaming issues. *)
+
+let keywords =
+ List.fold_right Idset.add
+ [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
+ "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
+ "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
+ "inherit"; "initializer"; "lazy"; "let"; "match"; "method";
+ "module"; "mutable"; "new"; "object"; "of"; "open"; "or";
+ "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
+ "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
+ "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
+ Idset.empty
+;;
+
+set_keywords keywords;;
+
+let pp_open status filename =
+ let status,res = modname_of_filename status true filename in
+ status, str ("open " ^ res ^ "\n") ++ fnl ()
+
+(*s The pretty-printer for Ocaml syntax*)
+
+(* Beware of the side-effects of [pp_global] and [pp_modname].
+ They are used to update table of content for modules. Many [let]
+ below should not be altered since they force evaluation order.
+*)
+
+let str_global status k r =
+ (*CSC: if is_inline_custom r then find_custom r else*) Common.pp_global status k r
+
+let pp_global status k r =
+ let status,res = str_global status k r in
+ status,str res
+
+(*CSC
+let pp_modname mp = str (Common.pp_module mp)
+
+let is_infix r =
+ is_inline_custom r &&
+ (let s = find_custom r in
+ let l = String.length s in
+ l >= 2 && s.[0] = '(' && s.[l-1] = ')')
+
+let get_infix r =
+ let s = find_custom r in
+ String.sub s 1 (String.length s - 2)
+*)
+
+let pp_one_field status _r _i r = pp_global status Term r
+
+let pp_field status r fields i = pp_one_field status r i (List.nth fields i)
+
+let pp_fields status r fields =
+ list_map_i_status status (fun status -> pp_one_field status r) 0 fields
+
+(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
+ are needed or not. *)
+
+let rec pp_type status par vl t =
+ let rec pp_rec status par = function
+ | Tmeta _ | Tvar' _ | Taxiom -> assert false
+ | Tvar i -> (try status,pp_tvar (List.nth vl (pred i))
+ with _ -> status,(str "'a" ++ int i))
+(*CSC:
+ | Tglob (r,[a1;a2]) when is_infix r ->
+ pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2)
+*)
+ | Tglob (r,[]) -> pp_global status Type r
+(*CSC:
+ | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" ->
+ pp_tuple_light pp_rec l
+*)
+ | Tglob (r,l) ->
+ let status,res = pp_tuple_light status pp_rec l in
+ let status,res2 = pp_global status Type r in
+ status,res ++ spc () ++ res2
+ | Tarr (t1,t2) ->
+ let status,res = pp_rec status true t1 in
+ let status,res2 = pp_rec status false t2 in
+ status,pp_par par (res ++ spc () ++ str "->" ++ spc () ++ res2)
+ | Tdummy _ -> status,str "__"
+ | Tunknown -> status,str "__"
+ in
+ let status,res = pp_rec status par t in
+ status,hov 0 res
+
+(*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 is_ifthenelse = function
+(*CSC:
+ | [|(r1,[],_);(r2,[],_)|] ->
+ (try (find_custom r1 = "true") && (find_custom r2 = "false")
+ with Not_found -> false)*)
+ | _ -> false
+
+let expr_needs_par = function
+ | MLlam _ -> true
+ | MLcase (_,_,[|_|]) -> false
+ | MLcase (_,_,pv) -> not (is_ifthenelse pv)
+ | _ -> false
+
+let rec pp_expr status par env args =
+ let par' = args <> [] || par
+ and apply st = pp_apply st par args in
+ function
+ | MLrel n ->
+ let id = get_db_name n env in status,apply (pr_id id)
+ | MLapp (f,args') ->
+ let status,stl = map_status status (fun status -> pp_expr status true env []) args' in
+ pp_expr status par env (stl @ args) f
+ | MLlam _ as a ->
+ let fl,a' = collect_lams a in
+ let fl = List.map id_of_mlid fl in
+ let fl,env' = push_vars fl env in
+ let status,res = pp_expr status false env' [] a' in
+ let st = (pp_abst (List.rev fl) ++ res) in
+ status,apply (pp_par par' st)
+ | MLletin (id,a1,a2) ->
+ let i,env' = push_vars [id_of_mlid id] env in
+ let pp_id = pr_id (List.hd i) in
+ let status,pp_a1 = pp_expr status false env [] a1 in
+ let status,pp_a2 =
+ pp_expr status (not par && expr_needs_par a2) env' [] a2 in
+ status,
+ hv 0
+ (apply
+ (pp_par par'
+ (hv 0
+ (hov 2
+ (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
+ spc () ++ str "in") ++
+ spc () ++ hov 0 pp_a2)))
+ | MLglob r ->
+ (try
+ let args = list_skipn (projection_arity status r) args in
+ let record = List.hd args in
+ let status,res = pp_global status Term r in
+ status,pp_apply (record ++ str "." ++ res) par (List.tl args)
+ with _ ->
+ let status,res = pp_global status Term r in
+ status,apply res)
+(*CSC: | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c*)
+ | MLcons ({c_kind = Coinductive},r,[]) ->
+ assert (args=[]);
+ let status,res = pp_global status Cons r in
+ status,pp_par par (str "lazy " ++ res)
+ | MLcons ({c_kind = Coinductive},r,args') ->
+ assert (args=[]);
+ let status,tuple =
+ pp_tuple status (fun status -> pp_expr status true env []) args' in
+ let status,res = pp_global status Cons r in
+ status,
+ pp_par par (str "lazy (" ++ res ++ spc() ++ tuple ++str ")")
+ | MLcons (_,r,[]) ->
+ assert (args=[]);
+ pp_global status Cons r
+ | MLcons ({c_kind = Record fields}, r, args') ->
+ assert (args=[]);
+ let status,res = pp_fields status r fields in
+ let status,res2 =
+ map_status status (fun status -> pp_expr status true env []) args' in
+ status,pp_record_pat (res, res2)
+(*CSC: | MLcons (_,r,[arg1;arg2]) when is_infix r ->
+ assert (args=[]);
+ pp_par par
+ ((pp_expr status true env [] arg1) ++ str (get_infix r) ++
+ (pp_expr status true env [] arg2))*)
+ | MLcons (_,r,args') ->
+ assert (args=[]);
+ let status,tuple =
+ pp_tuple status (fun status -> pp_expr status true env []) args' in
+ let status,res = str_global status Cons r in
+ if res = "" (* hack Extract Inductive prod *)
+ then status,tuple
+ else
+ let status,res = pp_global status Cons r in
+ status,pp_par par (res ++ spc () ++ tuple)
+(*CSC: | MLcase (_, t, pv) when is_custom_match pv ->
+ let mkfun (_,ids,e) =
+ if ids <> [] then named_lams (List.rev ids) e
+ else dummy_lams (ast_lift 1 e) 1
+ in
+ apply
+ (pp_par par'
+ (hov 2
+ (str (find_custom_match pv) ++ fnl () ++
+ prvect (fun tr -> pp_expr status true env [] (mkfun tr) ++ fnl ()) pv
+ ++ pp_expr status true env [] t)))*)
+ | MLcase (info, t, pv) ->
+ let status,expr = if info.m_kind = Coinductive then
+ let status,res = pp_expr status true env [] t in
+ status,(str "Lazy.force" ++ spc () ++ res)
+ else
+ (pp_expr status false env [] t)
+ in
+ (try
+ (* First, can this match be printed as a mere record projection ? *)
+ let fields =
+ match info.m_kind with Record f -> f | _ -> raise Impossible
+ in
+ let (r, ids, c) = pv.(0) in
+ let n = List.length ids in
+ let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
+ let proj_hd status i =
+ let status,res = pp_expr status true env [] t in
+ let status,res2 = pp_field status r fields i in
+ status,res ++ str "." ++ res2
+ in
+ match c with
+ | MLrel i when i <= n ->
+ let status,res = proj_hd status (n-i) in
+ status,apply (pp_par par' res)
+ | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
+ let _ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
+ let status,res = proj_hd status (n-i) in
+ let status,res2 =
+ map_status status (fun status -> pp_expr status true env' []) a
+ in
+ status,(pp_apply res par (res2 @ args))
+ | _ -> raise Impossible
+ with Impossible ->
+ (* Second, can this match be printed as a let-in ? *)
+ if Array.length pv = 1 then
+ let status,s1,s2 = pp_one_pat status env info pv.(0) in
+ status,
+ apply
+ (hv 0
+ (pp_par par'
+ (hv 0
+ (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
+ ++ spc () ++ str "in") ++
+ spc () ++ hov 0 s2)))
+ else
+ let status,res =
+ try status,pp_ifthenelse par' env expr pv
+ with Not_found ->
+ let status,res = pp_pat status env info pv in
+ status,
+ v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ res)
+ in
+ (* Otherwise, standard match *)
+ status,
+ apply (pp_par par' res))
+ | MLfix (i,ids,defs) ->
+ let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+ pp_fix status par env' i (Array.of_list (List.rev ids'),defs) args
+ | MLexn s ->
+ (* An [MLexn] may be applied, but I don't really care. *)
+ status,pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
+ | MLdummy ->
+ status,str "__" (*An [MLdummy] may be applied, but I don't really care.*)
+ | MLmagic a ->
+ let status,res = pp_expr status true env [] a in
+ status,pp_apply (str "Obj.magic") par (res :: args)
+ | MLaxiom ->
+ status,pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
+
+
+and pp_record_pat (fields, args) =
+ str "{ " ++
+ prlist_with_sep (fun () -> str ";" ++ spc ())
+ (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
+ (List.combine fields args) ++
+ str " }"
+
+and pp_ifthenelse _par _env _expr pv = match pv with
+(*CSC: | [|(tru,[],the);(fal,[],els)|] when
+ (find_custom tru = "true") && (find_custom fal = "false")
+ ->
+ hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
+ hov 2 (str "then " ++
+ hov 2 (pp_expr status (expr_needs_par the) env [] the)) ++ spc () ++
+ hov 2 (str "else " ++
+ hov 2 (pp_expr status (expr_needs_par els) env [] els)))*)
+ | _ -> raise Not_found
+
+and pp_one_pat status env info (r,ids,t) =
+ let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
+ let status,expr = pp_expr status (expr_needs_par t) env' [] t in
+ let status,patt = match info.m_kind with
+ | Record fields ->
+ let status,res = pp_fields status r fields in
+ status,pp_record_pat (res, List.rev_map pr_id ids)
+ | _ -> match List.rev ids with
+(*CSC: | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2*)
+ | [] -> pp_global status Cons r
+ | ids ->
+ (* hack Extract Inductive prod *)
+ let status,res = str_global status Cons r in
+ let status,res2 =
+ if res = "" then status,mt()
+ else
+ let status,res = pp_global status Cons r in
+ status, res ++ spc () in
+ status,res2 ++ pp_boxed_tuple pr_id ids
+ in
+ status, patt, expr
+
+and pp_pat status env info pv =
+ let factor_br, factor_set = try match info.m_same with
+ | BranchFun ints ->
+ let i = Intset.choose ints in
+ branch_as_fun info.m_typs pv.(i), ints
+ | BranchCst ints ->
+ let i = Intset.choose ints in
+ ast_pop (branch_as_cst pv.(i)), ints
+ | BranchNone -> MLdummy, Intset.empty
+ with _ -> MLdummy, Intset.empty
+ in
+ let last = Array.length pv - 1 in
+ let status,res =
+ prvecti_status status
+ (fun status i x -> if Intset.mem i factor_set then status,mt () else
+ let status,s1,s2 = pp_one_pat status env info x in
+ status,
+ hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
+ if i = last && Intset.is_empty factor_set then mt () else fnl ())
+ pv
+ in
+ let status,res2 =
+ if Intset.is_empty factor_set then status,mt () else
+ let par = expr_needs_par factor_br in
+ match info.m_same with
+ | BranchFun _ ->
+ let ids, env' = push_vars [anonymous_name] env in
+ let status,res = pp_expr status par env' [] factor_br in
+ status,hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
+ hov 2 res)
+ | BranchCst _ ->
+ let status,res = pp_expr status par env [] factor_br in
+ status,hv 2 (str "| _ ->" ++ spc () ++ hov 2 res)
+ | BranchNone -> status,mt ()
+ in
+ status, res ++ res2
+
+and pp_function status env t =
+ let bl,t' = collect_lams t in
+ let bl,env' = push_vars (List.map id_of_mlid bl) env in
+ match t' with
+ | MLcase(i,MLrel 1,pv) when
+ i.m_kind = Standard (*CSC:&& not (is_custom_match pv)*) ->
+ if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
+ let status,res = pp_pat status env' i pv in
+ status,pr_binding (List.rev (List.tl bl)) ++
+ str " = function" ++ fnl () ++ v 0 res
+ else
+ let status,res = pp_pat status env' i pv in
+ status,
+ pr_binding (List.rev bl) ++
+ str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+ v 0 res
+ | _ ->
+ let status,res = pp_expr status false env' [] t' in
+ status,
+ pr_binding (List.rev bl) ++
+ str " =" ++ fnl () ++ str " " ++
+ hov 2 res
+
+(*s names of the functions ([ids]) are already pushed in [env],
+ and passed here just for convenience. *)
+
+and pp_fix status par env i (ids,bl) args =
+ let status,res =
+ prvect_with_sep_status status
+ (fun () -> fnl () ++ str "and ")
+ (fun status (fi,ti) ->
+ let status,res = pp_function status env ti in
+ status, pr_id fi ++ res)
+ (array_map2 (fun id b -> (id,b)) ids bl)
+ in
+ status,
+ pp_par par
+ (v 0 (str "let rec " ++ res ++ fnl () ++
+ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+
+let pp_val status e typ =
+ let status,res = pp_type status false [] typ in
+ status,
+ hov 4 (str "(** val " ++ e ++ str " :" ++ spc ()++res++ str " **)") ++ fnl2 ()
+
+(*s Pretty-printing of [Dfix] *)
+
+let pp_Dfix status (rv,c,t) =
+ let status,names = array_map_status status
+ (fun status r -> (*CSC:if is_inline_custom r then mt () else*) pp_global status Term r) rv
+ in
+ let rec pp status init i =
+ if i >= Array.length rv then
+ (if init then failwith "empty phrase" else status,mt ())
+ else
+ let void = false(*CSC:is_inline_custom rv.(i)*) ||
+ (not false(*CSC:(is_custom rv.(i))*) && c.(i) = MLexn "UNUSED")
+ in
+ if void then pp status init (i+1)
+ else
+ let status,def =
+ (*CSC:if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i))
+ else*) pp_function status (empty_env status) c.(i) in
+ let status,res = pp_val status names.(i) t.(i) in
+ let status,res2 = pp status false (i+1) in
+ status,
+ (if init then mt () else fnl2 ()) ++ res ++
+ str (if init then "let rec " else "and ") ++ names.(i) ++ def ++ res2
+ in pp status true 0
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let pp_comment s = str "(* " ++ s ++ str " *)"
+
+let pp_one_ind status prefix pl name cnames ctyps =
+ let pl = rename_tvars keywords pl in
+ let pp_constructor status i typs =
+ let status,res =
+ prlist_with_sep_status status
+ (fun () -> spc () ++ str "* ") (fun status -> pp_type status true pl) typs
+ in
+ status,
+ (if i=0 then mt () else fnl ()) ++
+ hov 3 (str "| " ++ cnames.(i) ++
+ (if typs = [] then mt () else str " of ") ++ res) in
+ let status,res =
+ if Array.length ctyps = 0 then status,str " unit (* empty inductive *)"
+ else
+ let status,res = prvecti_status status pp_constructor ctyps in
+ status, fnl () ++ v 0 res
+ in
+ status,
+ pp_parameters pl ++ str prefix ++ name ++
+ str " =" ++ res
+
+let pp_logical_ind packet =
+ pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+ fnl () ++
+ pp_comment (str "with constructors : " ++
+ prvect_with_sep spc pr_id packet.ip_consnames) ++
+ fnl ()
+
+let pp_singleton status packet =
+ let status,name = pp_global status Type packet.ip_reference in
+ let l = rename_tvars keywords packet.ip_vars in
+ let status,res = pp_type status false l (List.hd packet.ip_types.(0)) in
+ status,
+ hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
+ res ++ fnl () ++
+ pp_comment (str "singleton inductive, whose constructor was " ++
+ pr_id packet.ip_consnames.(0)))
+
+let pp_record status fields packet =
+ let ind = packet.ip_reference in
+ let status,name = pp_global status Type ind in
+ let status,fieldnames = pp_fields status ind fields in
+ let l = List.combine fieldnames packet.ip_types.(0) in
+ let pl = rename_tvars keywords packet.ip_vars in
+ let status,res =
+ prlist_with_sep_status status (fun () -> str ";" ++ spc ())
+ (fun status (p,t) ->
+ let status,res = pp_type status true pl t in
+ status, p ++ str " : " ++ res) l in
+ status,
+ str "type " ++ pp_parameters pl ++ name ++ str " = { "++ hov 0 res ++ str " }"
+
+let pp_coind pl name =
+ let pl = rename_tvars keywords pl in
+ pp_parameters pl ++ name ++ str " = " ++
+ pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++
+ fnl() ++ str "and "
+
+let pp_ind status co ind =
+ let prefix = if co then "__" else "" in
+ let some = ref false in
+ let init= ref (str "type ") in
+ let status,names =
+ array_map_status status
+ (fun status p ->
+ if p.ip_logical then status,mt ()
+ else pp_global status Type p.ip_reference)
+ ind.ind_packets
+ in
+ let status,cnames =
+ array_map_status status
+ (fun status p -> if p.ip_logical then status,[||] else
+ array_mapi_status status
+ (fun status j _ -> pp_global status Cons p.ip_consreferences.(j))
+ p.ip_types)
+ ind.ind_packets
+ in
+ let rec pp status i =
+ if i >= Array.length ind.ind_packets then status,mt ()
+ else
+ let p = ind.ind_packets.(i) in
+ (*CSC:
+ let ip = assert false(*CSC: (mind_of_kn kn,i)*) in
+ if is_custom (IndRef ip) then pp (i+1)
+ else*) begin
+ some := true;
+ if p.ip_logical then
+ let status,res = pp status (i+1) in
+ status, pp_logical_ind p ++ res
+ else
+ let s = !init in
+ let status,res =
+ pp_one_ind
+ status prefix p.ip_vars names.(i) cnames.(i) p.ip_types in
+ let status,res2 = pp status (i+1) in
+ begin
+ init := (fnl () ++ str "and ");
+ status,
+ s ++
+ (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ res ++ res2
+ end
+ end
+ in
+ let st = pp status 0 in if !some then st else failwith "empty phrase"
+
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_mind status i =
+ match i.ind_kind with
+ | Singleton -> pp_singleton status i.ind_packets.(0)
+ | Coinductive -> pp_ind status true i
+ | Record fields -> pp_record status fields i.ind_packets.(0)
+ | Standard -> pp_ind status false i
+
+let pp_decl status = function
+(*CSC: | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase"
+ | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
+ | Dind i -> pp_mind status i
+ | Dtype (r, l, t) ->
+ let status,name = pp_global status Type r in
+ let l = rename_tvars keywords l in
+ let ids, (status, def) =
+(*CSC: try
+ let ids,s = find_type_custom r in
+ pp_string_parameters ids, str "=" ++ spc () ++ str s
+ with Not_found ->*)
+ pp_parameters l,
+ if t = Taxiom then status, str "(* AXIOM TO BE REALIZED *)"
+ else
+ let status,res = pp_type status false l t in
+ status, str "=" ++ spc () ++ res
+ in
+ status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+ | Dterm (r, a, t) ->
+ let status,name = pp_global status Term r in
+ let status,def =
+ (*if is_custom r then str (" = " ^ find_custom r)
+ else*) if is_projection status r then
+ status,
+ (prvect str (Array.make (projection_arity status r) " _")) ++
+ str " x = x." ++ name
+ else
+ let status,res = pp_function status (empty_env status) a in
+ status, res ++ mt ()
+ in
+ let status,res = pp_val status name t in
+ status, res ++ hov 0 (str "let " ++ name ++ def)
+ | Dfix (rv,defs,typs) ->
+ pp_Dfix status (rv,defs,typs)
+
+let pp_spec status = function
+(* | Sval (r,_) when is_inline_custom r -> failwith "empty phrase"
+ | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase"*)
+ | Sind i -> pp_mind status i
+ | Sval (r,t) ->
+ let status,def = pp_type status false [] t in
+ let status,name = pp_global status Term r in
+ status, hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def)
+ | Stype (r,vl,ot) ->
+ let status, name = pp_global status Type r in
+ let l = rename_tvars keywords vl in
+ let status, ids, def =
+(*CSC:
+ try
+ let ids, s = find_type_custom r in
+ pp_string_parameters ids, str "= " ++ str s
+ with Not_found ->*)
+ let ids = pp_parameters l in
+ match ot with
+ | None -> status, ids, mt ()
+ | Some Taxiom -> status, ids, str "(* AXIOM TO BE REALIZED *)"
+ | Some t ->
+ let status,res = pp_type status false l t in
+ status, ids, str "=" ++ spc () ++ res
+ in
+ status, hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
+
+let pp_decl status d =
+ try pp_decl status d with Failure "empty phrase" -> status, mt ()
+;;
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+open Coq
+open Miniml
+open OcamlExtractionTable
+
+val pp_decl : #status as 'status -> ml_decl -> 'status * std_ppcmds
+val pp_spec : #status as 'status -> ml_spec -> 'status * std_ppcmds
+val pp_open : #status as 'status -> string -> 'status * std_ppcmds
--- /dev/null
+open OcamlExtractionTable
+open Coq
+
+let print_ocaml_of_obj0 status ((_uri,_,_,_,_) as obj) =
+ try
+ let status,res,resl = Extraction.extract status obj in
+ let status,_ =
+ map_status status
+ (fun status ml ->
+ let status,cmds = Ocaml.pp_spec status ml in
+ print_ppcmds ~in_ml:false status (cmds ++ fnl () ++ fnl ());
+ status,()) resl in
+ match res with
+ None ->
+(* print_ppcmds status
+ (str("(* " ^ NUri.string_of_uri uri ^ " non informative *)\n")++ fnl ());*)
+ status
+ | Some ml ->
+ let status,std_ppcmds = Ocaml.pp_decl status ml in
+ print_ppcmds status ~in_ml:true (std_ppcmds ++ fnl ());
+ status
+ with
+ HExtlib.Localized (_,exn) ->
+ prerr_endline (Printexc.to_string exn); assert false
+
+let do_if_ocaml_set f status =
+ if try ignore (Helm_registry.get "extract_ocaml"); true
+ with Helm_registry.Key_not_found _ -> false
+ then f status else status
+
+let print_open status uris =
+ do_if_ocaml_set
+ (fun status ->
+ let status,uris =
+ map_status status
+ (fun status uri ->
+ let status,b = to_be_included status uri in
+ status, if b then Some uri else None
+ ) uris in
+ let uris = HExtlib.filter_map (fun x -> x) uris in
+ let fnames =
+ List.map (fun uri -> Filename.basename (NUri.string_of_uri uri)) uris in
+ let status,cmds = map_status status Ocaml.pp_open fnames in
+ List.iter (print_ppcmds status ~in_ml:true) cmds;
+ List.iter (print_ppcmds status ~in_ml:false) cmds;
+ status
+ ) status
+
+let print_ocaml_of_obj status cmds =
+ do_if_ocaml_set (fun status -> print_ocaml_of_obj0 status cmds) status
+
+let open_file status ~baseuri fname =
+ do_if_ocaml_set
+ (fun status -> OcamlExtractionTable.open_file status ~baseuri fname) status
+
+let close_file status =
+ do_if_ocaml_set OcamlExtractionTable.close_file status
--- /dev/null
+open OcamlExtractionTable
+
+(* These commands have an effect iff OCAML_EXTRACTION is set *)
+
+val print_open: #status as 'status -> NUri.uri list -> 'status
+val print_ocaml_of_obj: #status as 'status -> NCic.obj -> 'status
+val open_file: #status as 'status -> baseuri:string -> string -> 'status
+val close_file: #status as 'status -> 'status
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+open Coq
+open Miniml
+
+type info_el =
+ TypeInfo of NReference.reference * ml_schema
+ | TermInfo of NReference.reference * ml_decl
+ | InductiveInfo of NUri.uri * ml_ind
+ | GuessProjectionInfo of NUri.uri * int
+ | ConfirmProjectionInfo of NReference.reference
+ | RegisterId of string
+ | ReferenceNameInfo of NReference.reference * string
+ | RegisterModname of string
+ | ModnameInfo of string * string
+
+type info = info_el list
+
+type db =
+ ml_schema Refmap.t *
+ ml_decl Refmap.t *
+ ml_ind NUri.UriMap.t *
+ int NUri.UriMap.t *
+ int Refmap.t *
+ Idset.t *
+ string Refmap.t *
+ ((out_channel * Format.formatter) * (out_channel * Format.formatter)) option *
+ Idset.t *
+ string Stringmap.t *
+ Uriset.t *
+ string *
+ info
+
+let set_keywords,get_keywords =
+ let keywords = ref Idset.empty in
+ ((:=) keywords),(fun () -> !keywords)
+
+let preamble = "preamble.ml"
+let upreamble = "Preamble"
+let empty_info = []
+let empty_modset = Idset.add preamble Idset.empty
+let empty_db () =
+ Refmap.empty,Refmap.empty,NUri.UriMap.empty,NUri.UriMap.empty,Refmap.empty,get_keywords (),Refmap.empty,None,empty_modset,Stringmap.empty,Uriset.empty,"",empty_info
+
+let register_info (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
+ match info with
+ TypeInfo (ref,schema) ->
+ Refmap.add ref schema dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | TermInfo (ref,schema) ->
+ dbty,Refmap.add ref schema dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | InductiveInfo (uri,ind) ->
+ dbty,dbt,NUri.UriMap.add uri ind dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | GuessProjectionInfo (uri,n) ->
+ dbty,dbt,dbi,NUri.UriMap.add uri n dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | ConfirmProjectionInfo (NReference.Ref (uri,_) as ref) ->
+ (try
+ let n = NUri.UriMap.find uri dbgp in
+ let dbgp = NUri.UriMap.remove uri dbgp in
+ dbty,dbt,dbi,dbgp,Refmap.add ref n dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ with Not_found -> dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos)
+ | RegisterId s ->
+ dbty,dbt,dbi,dbgp,dbp,Idset.add s dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | ReferenceNameInfo (ref,name) ->
+ dbty,dbt,dbi,dbgp,dbp,dbids,Refmap.add ref name dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos
+ | RegisterModname s ->
+ dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,Idset.add s dbmn1,dbmn2,dbo,curi,infos
+ | ModnameInfo (s,name) ->
+ dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,Stringmap.add s name dbmn2,dbo,curi,infos
+
+let add_info_to_db (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) info =
+ dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,info::infos
+
+let register_and_add_info ?(dummy=false) status info =
+ let db = status#ocaml_extraction_db in
+ let db = register_info db info in
+ let db = if dummy then db else add_info_to_db db info in
+ status#set_ocaml_extraction_db db
+
+let register_infos = List.fold_left register_info
+
+let refresh_uri_in_type ~refresh_uri_in_reference =
+ let rec aux =
+ function
+ | Tarr (t1,t2) -> Tarr (aux t1, aux t2)
+ | Tglob (r,tl) -> Tglob (refresh_uri_in_reference r, List.map aux tl)
+ | Tmeta { id=id; contents=contents } ->
+ let contents' =
+ match contents with
+ None -> None
+ | Some typ -> Some (aux typ)
+ in
+ Tmeta { id=id; contents=contents' }
+ | t -> t
+ in
+ aux
+
+let refresh_uri_in_kind ~refresh_uri_in_reference =
+ function
+ Singleton
+ | Coinductive
+ | Standard as k -> k
+ | Record rl -> Record (List.map refresh_uri_in_reference rl)
+
+let refresh_uri_in_packet ~refresh_uri_in_reference
+ { ip_reference = r;
+ ip_consreferences = rs;
+ ip_typename = n;
+ ip_consnames = ns;
+ ip_logical = l;
+ ip_sign = s;
+ ip_vars = v;
+ ip_types = tys } =
+ { ip_reference = refresh_uri_in_reference r;
+ ip_consreferences = Array.map refresh_uri_in_reference rs;
+ ip_typename = n;
+ ip_consnames = ns;
+ ip_logical = l;
+ ip_sign = s;
+ ip_vars = v;
+ ip_types = Array.map (List.map (refresh_uri_in_type ~refresh_uri_in_reference)) tys }
+
+let refresh_uri_in_ind ~refresh_uri_in_reference
+ {ind_kind=k; ind_nparams=n; ind_packets=pa}
+=
+ let k = refresh_uri_in_kind ~refresh_uri_in_reference k in
+ let pa = Array.map (refresh_uri_in_packet ~refresh_uri_in_reference) pa in
+ {ind_kind=k; ind_nparams=n; ind_packets=pa}
+
+let refresh_uri_in_ast ~refresh_uri_in_reference =
+ let rec aux =
+ function
+ | MLapp (t,tl) -> MLapp (aux t, List.map aux tl)
+ | MLlam (id,t) -> MLlam (id, aux t)
+ | MLletin (id,t1,t2) -> MLletin (id, aux t1, aux t2)
+ | MLglob r -> MLglob (refresh_uri_in_reference r)
+ | MLcons ({c_kind=ckind; c_typs=ctyps}, r, tl) ->
+ let cinfo =
+ {c_kind=refresh_uri_in_kind ~refresh_uri_in_reference ckind;
+ c_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) ctyps}
+ in
+ MLcons (cinfo, refresh_uri_in_reference r, List.map aux tl)
+ | MLcase ({m_kind=k; m_typs=typs; m_same=same},t,ba) ->
+ let info =
+ {m_kind=refresh_uri_in_kind ~refresh_uri_in_reference k;
+ m_typs=List.map (refresh_uri_in_type ~refresh_uri_in_reference) typs;
+ m_same=same} in
+ let ba =
+ Array.map
+ (fun (r,il,t) -> refresh_uri_in_reference r,il,aux t) ba in
+ MLcase (info,aux t,ba)
+ | MLfix (n,ida,ta) -> MLfix (n,ida,Array.map aux ta)
+ | MLmagic t -> MLmagic (aux t)
+ | MLrel _
+ | MLexn _
+ | MLdummy
+ | MLaxiom as t -> t
+ in
+ aux
+
+let refresh_uri_in_decl ~refresh_uri_in_reference =
+ function
+ Dind ind -> Dind (refresh_uri_in_ind ~refresh_uri_in_reference ind)
+ | Dtype (ref,il,ty) ->
+ Dtype
+ (refresh_uri_in_reference ref, il,
+ refresh_uri_in_type ~refresh_uri_in_reference ty)
+ | Dterm (ref,ast,ty) ->
+ Dterm
+ (refresh_uri_in_reference ref,
+ refresh_uri_in_ast ~refresh_uri_in_reference ast,
+ refresh_uri_in_type ~refresh_uri_in_reference ty)
+ | Dfix (refa, asta, tya) ->
+ Dfix
+ (Array.map refresh_uri_in_reference refa,
+ Array.map (refresh_uri_in_ast ~refresh_uri_in_reference) asta,
+ Array.map (refresh_uri_in_type ~refresh_uri_in_reference) tya)
+
+let refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri =
+ function
+ TypeInfo (ref,(n,typ)) ->
+ TypeInfo
+ (refresh_uri_in_reference ref,
+ (n,refresh_uri_in_type ~refresh_uri_in_reference typ))
+ | TermInfo (ref,decl) ->
+ TermInfo
+ (refresh_uri_in_reference ref,
+ refresh_uri_in_decl ~refresh_uri_in_reference decl)
+ | InductiveInfo (uri,ind) ->
+ InductiveInfo
+ (refresh_uri uri, refresh_uri_in_ind ~refresh_uri_in_reference ind)
+ | GuessProjectionInfo (uri,n) ->
+ GuessProjectionInfo (refresh_uri uri, n)
+ | ConfirmProjectionInfo ref ->
+ ConfirmProjectionInfo (refresh_uri_in_reference ref)
+ | RegisterId s -> RegisterId s
+ | ReferenceNameInfo (ref,name) ->
+ ReferenceNameInfo (refresh_uri_in_reference ref,name)
+ | RegisterModname s -> RegisterModname s
+ | ModnameInfo (s,name) -> ModnameInfo (s,name)
+
+let refresh_uri_in_info ~refresh_uri_in_reference ~refresh_uri infos =
+ List.map
+ (refresh_uri_in_info_el ~refresh_uri_in_reference ~refresh_uri)
+ infos
+
+class type g_status =
+ object ('self)
+ method ocaml_extraction_db: db
+ method get_info: info * 'self
+ end
+
+class virtual status =
+ object (self)
+ inherit NCic.status
+ val ocaml_extraction_db = empty_db ()
+ method ocaml_extraction_db = ocaml_extraction_db
+ method get_info =
+ let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = self#ocaml_extraction_db in
+ infos,{< ocaml_extraction_db =
+ db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,empty_info >}
+ method set_ocaml_extraction_db v = {< ocaml_extraction_db = v >}
+ method set_ocaml_extraction_status
+ : 'status. #g_status as 'status -> 'self
+ = fun o -> {< ocaml_extraction_db = o#ocaml_extraction_db >}
+ end
+
+let open_file status ~baseuri filename =
+ let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,_,infos = status#ocaml_extraction_db in
+ assert (ch=None);
+ let chml = open_out filename in
+ let chml = chml,Format.formatter_of_out_channel chml in
+ let chmli = open_out (filename ^ "i") in
+ let chmli = chmli,Format.formatter_of_out_channel chmli in
+ pp_with (snd chml) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
+ pp_with (snd chmli) (str ("open " ^ upreamble ^ "\n") ++ fnl ());
+ let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,Some (chml,chmli),dbmn1,dbmn2,dbo,baseuri,infos in
+ status#set_ocaml_extraction_db db
+
+let close_file status =
+ let db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos = status#ocaml_extraction_db in
+ match ch with
+ None -> assert false
+ | Some ch ->
+ close_out (fst (fst ch));
+ close_out (fst (snd ch));
+ let ch = None in
+ let db = db1,db2,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos in
+ status#set_ocaml_extraction_db db
+
+let print_ppcmds status ~in_ml cmds =
+ let _,_,_,_,_,_,_,ch,_,_,_,_,_ = status#ocaml_extraction_db in
+ match ch with
+ None -> assert false
+ | Some ch ->
+ let ch = if in_ml then fst ch else snd ch in
+ pp_with (snd ch) cmds
+
+let to_be_included status uri =
+ let dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos =
+ status#ocaml_extraction_db
+ in
+ if Uriset.mem uri dbo then
+ status,false
+ else
+ let dbo = Uriset.add uri dbo in
+ let status =
+ status#set_ocaml_extraction_db
+ (dbty,dbt,dbi,dbgp,dbp,dbids,dbrefs,ch,dbmn1,dbmn2,dbo,curi,infos) in
+ status,true
+
+let add_term status ref decl =
+ let info = TermInfo (ref,decl) in
+ register_and_add_info status info
+
+let lookup_term status ref =
+ let _,dbt,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ Refmap.find ref dbt
+
+let add_type status ref schema =
+ let info = TypeInfo (ref,schema) in
+ register_and_add_info status info
+
+let lookup_type status ref =
+ let dbty,_,_,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ Refmap.find ref dbty
+
+let add_name_for_reference status ref name =
+ let info = ReferenceNameInfo (ref,name) in
+ register_and_add_info status info
+
+let name_of_reference status ref =
+ let _,_,_,_,_,_,dbrefs,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ Refmap.find ref dbrefs
+
+let add_modname_for_filename status ref name =
+ let info = ModnameInfo (ref,name) in
+ register_and_add_info status info
+
+let modname_of_filename status ref =
+ let _,_,_,_,_,_,_,_,_,dbmn2,_,_,_ = status#ocaml_extraction_db in
+ Stringmap.find ref dbmn2
+
+let add_global_ids status id =
+ let info = RegisterId id in
+ register_and_add_info status info
+
+let get_global_ids status =
+ let _,_,_,_,_,dbids,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ dbids
+
+let add_modname status id =
+ let info = RegisterModname id in
+ register_and_add_info status info
+
+let get_modnames status =
+ let _,_,_,_,_,_,_,_,dbmn1,_,_,_,_ = status#ocaml_extraction_db in
+ dbmn1
+
+let add_ind status ?dummy uri ind =
+ let info = InductiveInfo (uri,ind) in
+ register_and_add_info ?dummy status info
+
+let lookup_ind status uri =
+ let _,_,dbi,_,_,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ NUri.UriMap.find uri dbi
+
+let current_baseuri status =
+ let _,_,_,_,_,_,_,_,_,_,_,suri,_ = status#ocaml_extraction_db in suri
+
+let guess_projection status ref n =
+ let info = GuessProjectionInfo (ref,n) in
+ register_and_add_info status info
+
+let confirm_projection status ref =
+ let info = ConfirmProjectionInfo ref in
+ register_and_add_info status info
+
+let is_projection status ref =
+ let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ Refmap.mem ref dbp
+
+let projection_arity status ref =
+ let _,_,_,_,dbp,_,_,_,_,_,_,_,_ = status#ocaml_extraction_db in
+ Refmap.find ref dbp
+
+let type_expand () = true
+
+(*s Extraction Optimize *)
+
+type opt_flag =
+ { opt_kill_dum : bool; (* 1 *)
+ opt_fix_fun : bool; (* 2 *)
+ opt_case_iot : bool; (* 4 *)
+ opt_case_idr : bool; (* 8 *)
+ opt_case_idg : bool; (* 16 *)
+ opt_case_cst : bool; (* 32 *)
+ opt_case_fun : bool; (* 64 *)
+ opt_case_app : bool; (* 128 *)
+ opt_let_app : bool; (* 256 *)
+ opt_lin_let : bool; (* 512 *)
+ opt_lin_beta : bool } (* 1024 *)
+
+let kth_digit n k = (n land (1 lsl k) <> 0)
+
+let flag_of_int n =
+ { opt_kill_dum = kth_digit n 0;
+ opt_fix_fun = kth_digit n 1;
+ opt_case_iot = kth_digit n 2;
+ opt_case_idr = kth_digit n 3;
+ opt_case_idg = kth_digit n 4;
+ opt_case_cst = kth_digit n 5;
+ opt_case_fun = kth_digit n 6;
+ opt_case_app = kth_digit n 7;
+ opt_let_app = kth_digit n 8;
+ opt_lin_let = kth_digit n 9;
+ opt_lin_beta = kth_digit n 10 }
+
+(* For the moment, we allow by default everything except :
+ - the type-unsafe optimization [opt_case_idg], which anyway
+ cannot be activated currently (cf [Mlutil.branch_as_fun])
+ - the linear let and beta reduction [opt_lin_let] and [opt_lin_beta]
+ (may lead to complexity blow-up, subsumed by finer reductions
+ when inlining recursors).
+*)
+
+let int_flag_init = 1 + 2 + 4 + 8 (*+ 16*) + 32 + 64 + 128 + 256 (*+ 512 + 1024*)
+
+let opt_flag_ref = ref (flag_of_int int_flag_init)
+
+let optims () = !opt_flag_ref
--- /dev/null
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
+
+open Coq
+open Miniml
+
+type info
+type db
+
+class type g_status =
+ object ('self)
+ method ocaml_extraction_db: db
+ method get_info: info * 'self
+ end
+
+class virtual status :
+ object ('self)
+ inherit g_status
+ inherit NCic.status
+ method set_ocaml_extraction_db: db -> 'self
+ method set_ocaml_extraction_status: #g_status -> 'self
+ end
+
+val refresh_uri_in_info:
+ refresh_uri_in_reference:(NReference.reference -> NReference.reference) ->
+ refresh_uri:(NUri.uri -> NUri.uri) ->
+ info -> info
+
+val set_keywords : Idset.t -> unit
+
+val register_infos: db -> info -> db
+
+val to_be_included : #status as 'status -> NUri.uri -> 'status * bool
+
+val open_file: #status as 'status -> baseuri:string -> string -> 'status
+val print_ppcmds : #status -> in_ml:bool -> std_ppcmds -> unit
+val close_file: #status as 'status -> 'status
+
+val current_baseuri: #status -> string
+
+val add_term : #status as 'status -> NReference.reference -> ml_decl -> 'status
+val lookup_term : #status -> NReference.reference -> ml_decl
+
+val add_type: #status as 'status -> NReference.reference -> ml_schema -> 'status
+val lookup_type : #status -> NReference.reference -> ml_schema
+
+val add_ind : #status as 'status -> ?dummy:bool -> NUri.uri -> ml_ind -> 'status
+val lookup_ind : #status -> NUri.uri -> ml_ind
+
+val add_global_ids: #status as 'status -> string -> 'status
+val get_global_ids : #status -> Idset.t
+
+val add_name_for_reference:
+ #status as 'status -> NReference.reference -> string -> 'status
+val name_of_reference : #status -> NReference.reference -> string
+
+val add_modname: #status as 'status -> string -> 'status
+val get_modnames : #status -> Idset.t
+
+val add_modname_for_filename:
+ #status as 'status -> string -> string -> 'status
+val modname_of_filename : #status -> string -> string
+
+val guess_projection:
+ #status as 'status -> NUri.uri -> int -> 'status
+val confirm_projection:
+ #status as 'status -> NReference.reference -> 'status
+val is_projection : #status -> NReference.reference -> bool
+val projection_arity : #status -> NReference.reference -> int
+
+val type_expand : unit -> bool
+
+type opt_flag =
+ { opt_kill_dum : bool; (* 1 *)
+ opt_fix_fun : bool; (* 2 *)
+ opt_case_iot : bool; (* 4 *)
+ opt_case_idr : bool; (* 8 *)
+ opt_case_idg : bool; (* 16 *)
+ opt_case_cst : bool; (* 32 *)
+ opt_case_fun : bool; (* 64 *)
+ opt_case_app : bool; (* 128 *)
+ opt_let_app : bool; (* 256 *)
+ opt_lin_let : bool; (* 512 *)
+ opt_lin_beta : bool } (* 1024 *)
+
+val optims : unit -> opt_flag
projects / helm.git / commitdiff