| KSkip k -> size_of_kind k
;;
-let bracket size_of pp o =
- if size_of o > 1 then
+let bracket ?(prec=1) size_of pp o =
+ if size_of o > prec then
"(" ^ pp o ^ ")"
else
pp o
let rec size_of_type =
function
- | Var _ -> 1
- | Unit -> 1
- | Top -> 1
- | TConst _ -> 1
+ | Var _ -> 0
+ | Unit -> 0
+ | Top -> 0
+ | TConst _ -> 0
| Arrow _ -> 2
| TSkip t -> size_of_type t
| Forall _ -> 2
module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
-type info_el = typ_context * typ option
+module GlobalNames = Set.Make(String)
+
+type info_el =
+ string * [`Type of typ_context * typ option | `Constructor | `Function ]
type info = (NReference.reference * info_el) list
-type db = info_el ReferenceMap.t
+type db = info_el ReferenceMap.t * GlobalNames.t
let empty_info = []
-let register_info db (ref,info) = ReferenceMap.add ref info db
-
-let register_infos = List.fold_left register_info
-
type obj_kind =
TypeDeclaration of typ_former_decl
| TypeDefinition of typ_former_def
class virtual status =
object
inherit NCic.status
- val extraction_db = ReferenceMap.empty
+ val extraction_db = ReferenceMap.empty, GlobalNames.empty
method extraction_db = extraction_db
method set_extraction_db v = {< extraction_db = v >}
method set_extraction_status
| 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 List.rev (fst (ReferenceMap.find ref status#extraction_db))
+ (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 *)
+ backbone. That is why we can safely return the dummy context
+ here *)
let rec dummy = None::dummy in
dummy)
| NCic.Match _ -> assert false (* TODO ???? *)
| Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t)
| TAppl args -> TAppl (List.map (fomega_subst k t1) args)
-let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db)
+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
| 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 ->
ctx0 ctx
in
let bo = typ_of status ~metasenv ctx bo in
- let info = ref,(nicectx,Some bo) in
- status#set_extraction_db
- (register_info status#extraction_db info),
- Success ([info],ref,TypeDefinition((nicectx,res),bo))
+ 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
| `Proposition -> status, Erased
| `KindOrType (* ??? *)
| `Type ->
- (* CSC: TO BE FINISHED, REF NON REGISTERED *)
let ty = typ_of status ~metasenv [] ty in
+ let info = ref,`Function in
+ let status,info = register_name_and_info status info in
status,
- Success ([],ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo))
+ 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 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,(ctx,None) in
- let status =
- status#set_extraction_db
- (register_info status#extraction_db info) in
- let cl =
- HExtlib.list_mapi
- (fun (_,_,ty) j ->
+ 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
- NReference.mk_constructor (j+1) ref,ty
- ) cl
+ let ref = NReference.mk_constructor j ref in
+ let info = ref,`Constructor 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],ref,left,right,cl)::res
+ status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::res
) (status,0,[]) il
in
match rev_tyl with
| `Kind ->
let ty = kind_of status ~metasenv [] ty in
let ctx,_ as res = split_kind_prods [] ty in
- let info = ref,(ctx,None) in
- status#set_extraction_db
- (register_info status#extraction_db info),
- Success ([info],ref, TypeDeclaration res)
+ 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
- status, Success ([],ref, TermDeclaration (split_typ_prods [] ty))
+ let info = ref,`Function 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
* ----------------------------------------------------------------------------
*)
-let remove_underscores_and_mark =
+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)
else
aux (x::char_list_buffer) positions_buffer (position + 1) xs
in
- aux [] [] 0
+ if l = ['_'] then "_",[] else aux [] [] 0 l
;;
let rec capitalize_marked_positions s =
String.uncapitalize
;;
-(*CSC: code to be changed soon when we implement constructors and
- we fix the code for term application *)
let classify_reference status ref =
- if ReferenceMap.mem ref status#extraction_db then
- `TypeName
- else
- let NReference.Ref (_,r) = ref in
- match r with
- NReference.Con _ -> `Constructor
- | NReference.Ind _ -> assert false
- | _ -> `FunctionName
+ 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 =
let pp_ref status ref =
capitalize (classify_reference status ref)
- (NCicPp.r2s status true 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 =
function
| Var n -> List.nth ctxt (n-1)
| Unit -> "()"
- | Top -> "Top"
+ | Top -> "GHC.Prim.Any"
| TConst ref -> pp_ref status ref
| Arrow (t1,t2) ->
bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^
"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 (pretty_print_type status ctxt) tl)
+ | TAppl tl ->
+ String.concat " "
+ (List.map
+ (fun t -> bracket ~prec:0 size_of_type
+ (pretty_print_type status ctxt) t) tl)
let pretty_print_term_context status ctx1 ctx2 =
let name_context, rev_res =
let namectx = namectx_of_ctx left in
pp_ref status ref ^ " :: " ^
pretty_print_type status namectx tys
- ) cl) ^ "\n deriving (Prelude.Show)"
+ ) cl) (*^ "\n deriving (Prelude.Show)"*)
) il)
(* inductive and records missing *)
let refresh_uri_in_info ~refresh_uri_in_reference infos =
List.map
- (function (ref,(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,(ctx,typ))
+ (function (ref,el) ->
+ match el with
+ _,`Constructor
+ | _,`Function -> refresh_uri_in_reference ref,el
+ | 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
projects / helm.git / blobdiff