From 95e3387af669e9a9e30dafd4d096c2741fc9041c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 2 Feb 2013 00:38:55 +0000 Subject: [PATCH] Ooops, this completes the previous commit (ocaml extraction implementation). --- matita/components/ng_extraction/Makefile | 24 + matita/components/ng_extraction/common.ml | 158 ++ matita/components/ng_extraction/common.mli | 44 + matita/components/ng_extraction/coq.ml | 457 ++++++ matita/components/ng_extraction/coq.mli | 83 + matita/components/ng_extraction/extraction.ml | 1318 ++++++++++++++++ .../components/ng_extraction/extraction.mli | 19 + matita/components/ng_extraction/miniml.ml | 181 +++ matita/components/ng_extraction/mlutil.ml | 1333 +++++++++++++++++ matita/components/ng_extraction/mlutil.mli | 138 ++ .../ng_extraction/nCicExtraction.ml | 1270 ++++++++++++++++ .../ng_extraction/nCicExtraction.mli | 40 + matita/components/ng_extraction/ocaml.ml | 652 ++++++++ matita/components/ng_extraction/ocaml.mli | 17 + .../ng_extraction/ocamlExtraction.ml | 57 + .../ng_extraction/ocamlExtraction.mli | 8 + .../ng_extraction/ocamlExtractionTable.ml | 398 +++++ .../ng_extraction/ocamlExtractionTable.mli | 93 ++ 18 files changed, 6290 insertions(+) create mode 100644 matita/components/ng_extraction/Makefile create mode 100644 matita/components/ng_extraction/common.ml create mode 100644 matita/components/ng_extraction/common.mli create mode 100644 matita/components/ng_extraction/coq.ml create mode 100644 matita/components/ng_extraction/coq.mli create mode 100644 matita/components/ng_extraction/extraction.ml create mode 100644 matita/components/ng_extraction/extraction.mli create mode 100644 matita/components/ng_extraction/miniml.ml create mode 100644 matita/components/ng_extraction/mlutil.ml create mode 100644 matita/components/ng_extraction/mlutil.mli create mode 100644 matita/components/ng_extraction/nCicExtraction.ml create mode 100644 matita/components/ng_extraction/nCicExtraction.mli create mode 100644 matita/components/ng_extraction/ocaml.ml create mode 100644 matita/components/ng_extraction/ocaml.mli create mode 100644 matita/components/ng_extraction/ocamlExtraction.ml create mode 100644 matita/components/ng_extraction/ocamlExtraction.mli create mode 100644 matita/components/ng_extraction/ocamlExtractionTable.ml create mode 100644 matita/components/ng_extraction/ocamlExtractionTable.mli diff --git a/matita/components/ng_extraction/Makefile b/matita/components/ng_extraction/Makefile new file mode 100644 index 000000000..8bbda655e --- /dev/null +++ b/matita/components/ng_extraction/Makefile @@ -0,0 +1,24 @@ +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 diff --git a/matita/components/ng_extraction/common.ml b/matita/components/ng_extraction/common.ml new file mode 100644 index 000000000..57a27e92b --- /dev/null +++ b/matita/components/ng_extraction/common.ml @@ -0,0 +1,158 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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) diff --git a/matita/components/ng_extraction/common.mli b/matita/components/ng_extraction/common.mli new file mode 100644 index 000000000..4bde847ac --- /dev/null +++ b/matita/components/ng_extraction/common.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/matita/components/ng_extraction/coq.ml b/matita/components/ng_extraction/coq.ml new file mode 100644 index 000000000..f68562c20 --- /dev/null +++ b/matita/components/ng_extraction/coq.ml @@ -0,0 +1,457 @@ +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 + +(* ---- *) diff --git a/matita/components/ng_extraction/coq.mli b/matita/components/ng_extraction/coq.mli new file mode 100644 index 000000000..98639e8bb --- /dev/null +++ b/matita/components/ng_extraction/coq.mli @@ -0,0 +1,83 @@ +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 diff --git a/matita/components/ng_extraction/extraction.ml b/matita/components/ng_extraction/extraction.ml new file mode 100644 index 000000000..c186aef3c --- /dev/null +++ b/matita/components/ng_extraction/extraction.ml @@ -0,0 +1,1318 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/matita/components/ng_extraction/extraction.mli b/matita/components/ng_extraction/extraction.mli new file mode 100644 index 000000000..efb2c63da --- /dev/null +++ b/matita/components/ng_extraction/extraction.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* NCic.obj -> + 'status * ml_decl option * ml_spec list diff --git a/matita/components/ng_extraction/miniml.ml b/matita/components/ng_extraction/miniml.ml new file mode 100644 index 000000000..8fc795475 --- /dev/null +++ b/matita/components/ng_extraction/miniml.ml @@ -0,0 +1,181 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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; + +} diff --git a/matita/components/ng_extraction/mlutil.ml b/matita/components/ng_extraction/mlutil.ml new file mode 100644 index 000000000..0d5e89f6e --- /dev/null +++ b/matita/components/ng_extraction/mlutil.ml @@ -0,0 +1,1333 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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))) +*) diff --git a/matita/components/ng_extraction/mlutil.mli b/matita/components/ng_extraction/mlutil.mli new file mode 100644 index 000000000..a04dc2914 --- /dev/null +++ b/matita/components/ng_extraction/mlutil.mli @@ -0,0 +1,138 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/matita/components/ng_extraction/nCicExtraction.ml b/matita/components/ng_extraction/nCicExtraction.ml new file mode 100644 index 000000000..4e167004d --- /dev/null +++ b/matita/components/ng_extraction/nCicExtraction.ml @@ -0,0 +1,1270 @@ +(* 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 diff --git a/matita/components/ng_extraction/nCicExtraction.mli b/matita/components/ng_extraction/nCicExtraction.mli new file mode 100644 index 000000000..d5cb66360 --- /dev/null +++ b/matita/components/ng_extraction/nCicExtraction.mli @@ -0,0 +1,40 @@ +(* + ||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) diff --git a/matita/components/ng_extraction/ocaml.ml b/matita/components/ng_extraction/ocaml.ml new file mode 100644 index 000000000..a612c58d4 --- /dev/null +++ b/matita/components/ng_extraction/ocaml.ml @@ -0,0 +1,652 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '\'' + 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 () +;; diff --git a/matita/components/ng_extraction/ocaml.mli b/matita/components/ng_extraction/ocaml.mli new file mode 100644 index 000000000..c257804c0 --- /dev/null +++ b/matita/components/ng_extraction/ocaml.mli @@ -0,0 +1,17 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 diff --git a/matita/components/ng_extraction/ocamlExtraction.ml b/matita/components/ng_extraction/ocamlExtraction.ml new file mode 100644 index 000000000..1d672c49d --- /dev/null +++ b/matita/components/ng_extraction/ocamlExtraction.ml @@ -0,0 +1,57 @@ +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 diff --git a/matita/components/ng_extraction/ocamlExtraction.mli b/matita/components/ng_extraction/ocamlExtraction.mli new file mode 100644 index 000000000..a714bd13b --- /dev/null +++ b/matita/components/ng_extraction/ocamlExtraction.mli @@ -0,0 +1,8 @@ +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 diff --git a/matita/components/ng_extraction/ocamlExtractionTable.ml b/matita/components/ng_extraction/ocamlExtractionTable.ml new file mode 100644 index 000000000..148377e6f --- /dev/null +++ b/matita/components/ng_extraction/ocamlExtractionTable.ml @@ -0,0 +1,398 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* !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 diff --git a/matita/components/ng_extraction/ocamlExtractionTable.mli b/matita/components/ng_extraction/ocamlExtractionTable.mli new file mode 100644 index 000000000..6fdf4407a --- /dev/null +++ b/matita/components/ng_extraction/ocamlExtractionTable.mli @@ -0,0 +1,93 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* '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 -- 2.39.2