type typ =
Var of int
+ | Unit
| Top
| TConst of typformerreference
| Arrow of typ * typ
type term =
Rel of int
+ | UnitTerm
| Const of reference
| Lambda of string * (* typ **) term
| Appl of term list
| TypeDefinition of typ_former_def
| TermDeclaration of term_former_decl
| TermDefinition of term_former_def
- | LetRec of (string * typ * term) list
- (* inductive and records missing *)
+ | LetRec of obj_kind list
+ | Algebraic of (string * typ_context * (string * typ list) list) list
type obj = NUri.uri * obj_kind
assert false (* TODO *)
| NCic.Meta _ -> assert false (* TODO *)
| NCic.Appl (he::_) -> classify_not_term status no_dep_prods context he
- | NCic.Rel _ -> `KindOrType
- | NCic.Const (NReference.Ref (_,NReference.Decl _) as ref) ->
+ | 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 true [] ty with
| `Proposition
| `Type -> assert false (* IMPOSSIBLE *)
| `Kind
- | `KindOrType -> `KindOrType
+ | `KindOrType -> `Type
| `PropKind -> `Proposition)
| NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) ->
let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in
| `PropKind -> `Proposition)
| NCic.Const (NReference.Ref (_,NReference.Con _))
| NCic.Const (NReference.Ref (_,NReference.Def _)) ->
- assert false (* NOT POSSIBLE *)
+ assert false (* IMPOSSIBLE *)
;;
type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];;
(classify_not_term status true context t : not_term :> [> not_term])
| ty ->
let ty = fix_sorts ty in
-prerr_endline ("XXX: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty);
`Term
(match classify_not_term status true context ty with
| `Proposition -> `Proof
let rec kind_of status ~metasenv context k =
match NCicReduction.whd status ~subst:[] context k with
- | NCic.Sort _ -> Type
+ | NCic.Sort NCic.Type _ -> Type
+ | NCic.Sort _ -> assert false (* NOT A KIND *)
| NCic.Prod (b,s,t) ->
(* CSC: non-invariant assumed here about "_" *)
(match classify status ~metasenv context s with
match classify status ~metasenv context arg with
| `KindOrType
| `Type
- | `Term `TypeFormer -> arg::skip_args status ~metasenv context (tl1,tl2)
+ | `Term `TypeFormer ->
+ Some arg::skip_args status ~metasenv context (tl1,tl2)
| `Kind
| `Proposition
- | `PropKind -> unitty::skip_args status ~metasenv context (tl1,tl2)
+ | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2)
| `Term _ -> assert false (* IMPOSSIBLE *)
;;
module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end)
-type db = typ_context ReferenceMap.t
+type db = (typ_context * typ option) ReferenceMap.t
class type g_status =
object
| _ 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 (Skip typ)
+;;
+
let rec split_typ_lambdas status n ~metasenv context typ =
if n = 0 then context,typ
else
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.Decl) as ref)
| NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) ->
- (try ReferenceMap.find ref status#extraction_db
+ (try fst (ReferenceMap.find ref status#extraction_db)
with
Not_found -> assert false (* IMPOSSIBLE *))
| NCic.Match _ -> assert false (* TODO ???? *)
| NCic.Appl (he::args) ->
let he_context = context_of_typformer status ~metasenv context he in
TAppl (typ_of status ~metasenv context he ::
- List.map (typ_of status ~metasenv context)
+ List.map
+ (function None -> Unit | Some ty -> typ_of status ~metasenv context ty)
(skip_args status ~metasenv context (List.rev he_context,args)))
| NCic.Appl _ -> assert false (* TODO: when head is a match/let rec;
otherwise NOT A TYPE *)
| NCic.Match (_,_,_,_) -> assert false (* TODO *)
;;
+let rec fomega_subst k t1 =
+ function
+ | Var n ->
+ if k=n then 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)
+ | Skip t -> Skip (fomega_subst (k+1) t1 t)
+ | 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 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 term_of status ~metasenv context =
function
| NCic.Implicit _
| `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)
| `Proposition
| `Term `PropFormer
| `Term `TypeFormer
- | `Term `TypeFormerOrTerm
- | `Term `Proof -> assert false (* EXPAND IT ??? *))
+ | `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) ->
- assert false (* TODO
+ eat_args status metasenv
+ (term_of status ~metasenv context he) context
+ (typ_of status ~metasenv context
+ (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he))
+ args
+(*
let he_context = context_of_typformer status ~metasenv context he in
- TAppl (typ_of status ~metasenv context he ::
- List.map (typ_of status ~metasenv context)
- (skip_args status ~metasenv context (List.rev he_context,args)))*)
+ let process_args he =
+ function
+ `Empty -> he
+ | `Inst tl -> Inst (process_args he tl)
+ | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl
+ in
+ Appl (typ_of status ~metasenv context he ::
+ process_args (typ_of status ~metasenv context he)
+ (skip_term_args status ~metasenv context (List.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 *)
| NCic.Match (ref,_,t,pl) ->
Match (ref,term_of status ~metasenv context t,
List.map (term_of status ~metasenv context) pl)
+and eat_args status metasenv acc context tyhe =
+ function
+ [] -> acc
+ | arg::tl ->
+ let mk_appl f x =
+ match f with
+ Appl args -> Appl (args@[x])
+ | _ -> Appl [f;x]
+ in
+ match fomega_whd status tyhe with
+ Arrow (s,t) ->
+ let arg =
+ match s with
+ Unit -> UnitTerm
+ | _ -> term_of status ~metasenv context arg in
+ eat_args status metasenv (mk_appl acc arg) context t tl
+ | Forall (_,_,t) ->
+ eat_args status metasenv (Inst acc)
+ context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl
+ | Skip t ->
+ eat_args status metasenv acc context t tl
+ | Top -> assert false (*TODO: HOW??*)
+ | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *)
+;;
+
+let obj_of_constant status ~metasenv uri height 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
+ (* BUG here: for mutual type definitions the spec is not good *)
+ let ref =
+ NReference.reference_of_spec uri (NReference.Def height) in
+ let bo = typ_of status ~metasenv ctx bo in
+ status#set_extraction_db
+ (ReferenceMap.add ref (nicectx,Some bo)
+ status#extraction_db),
+ Some (uri,TypeDefinition((nicectx,res),bo))
+ | `Kind -> status, None
+ | `PropKind
+ | `Proposition -> status, None
+ | `Term _ -> assert false (* IMPOSSIBLE *))
+ | `PropKind
+ | `Proposition -> status, None
+ | `KindOrType (* ??? *)
+ | `Type ->
+ (* CSC: TO BE FINISHED, REF NON REGISTERED *)
+ let ty = typ_of status ~metasenv [] ty in
+ status,
+ Some (uri, TermDefinition (split_typ_prods [] ty,
+ term_of status ~metasenv [] bo))
+ | `Term _ -> assert false (* IMPOSSIBLE *)
+;;
+
+let obj_of_inductive status ~metasenv uri ind leftno il =
+ let tyl =
+ HExtlib.filter_map
+ (fun _,name,arity,cl ->
+ match classify_not_term status true [] arity with
+ | `Proposition
+ | `KindOrType
+ | `Type -> assert false (* IMPOSSIBLE *)
+ | `PropKind -> None
+ | `Kind ->
+ let arity = kind_of status ~metasenv [] arity in
+ let ctx,_ as res = split_kind_prods [] arity in
+ Some (name,ctx,[])
+ ) il
+ in
+ match tyl with
+ [] -> status,None
+ | _ -> status, Some (uri, Algebraic tyl)
;;
let obj_of status (uri,height,metasenv,subst,obj_kind) =
let ctx,_ as res = split_kind_prods [] ty in
let ref = NReference.reference_of_spec uri NReference.Decl in
status#set_extraction_db
- (ReferenceMap.add ref ctx status#extraction_db),
+ (ReferenceMap.add ref (ctx,None) status#extraction_db),
Some (uri, TypeDeclaration res)
- | `KindOrType -> assert false (* TODO ??? *)
| `PropKind
| `Proposition -> status, None
- | `Type ->
+ | `Type
+ | `KindOrType (*???*) ->
let ty = typ_of status ~metasenv [] ty in
status,
Some (uri, TermDeclaration (split_typ_prods [] ty))
| `Term _ -> assert false (* IMPOSSIBLE *))
| NCic.Constant (_,_,Some bo,ty,_) ->
- (match classify status ~metasenv [] ty with
- | `Kind ->
- let ty = kind_of status ~metasenv [] ty in
- let ctx0,_ as 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 ref =
- NReference.reference_of_spec uri (NReference.Def height) in
- status#set_extraction_db
- (ReferenceMap.add ref ctx0 status#extraction_db),
- Some (uri,TypeDefinition(res,typ_of status ~metasenv ctx bo))
- | `Kind -> status, None
- | `PropKind
- | `Proposition -> status, None
- | `Term _ -> assert false (* IMPOSSIBLE *))
- | `PropKind
- | `Proposition -> status, None
- | `KindOrType (* ??? *)
- | `Type ->
- (* CSC: TO BE FINISHED, REF NON REGISTERED *)
- let ty = typ_of status ~metasenv [] ty in
- status,
- Some (uri, TermDefinition (split_typ_prods [] ty,
- term_of status ~metasenv [](* BAD! *) bo))
- | `Term _ -> assert false (* IMPOSSIBLE *))
+ obj_of_constant status ~metasenv uri height bo ty
+ | NCic.Fixpoint (_fix_or_cofix,fs,_) ->
+ let status,objs =
+ List.fold_right
+ (fun (_,_name,_,ty,bo) (status,res) ->
+ let status,obj = obj_of_constant ~metasenv status uri height bo ty in
+ match obj with
+ None -> status,res (*CSC: PRETTY PRINT SOMETHING ERASED*)
+ | Some (_uri,obj) -> status,obj::res)
+ fs (status,[])
+ in
+ status, Some (uri,LetRec objs)
+ | NCic.Inductive (ind,leftno,il,_) ->
+ obj_of_inductive status ~metasenv uri ind leftno il
with
NotInFOmega ->
- prerr_endline "NOT IN F_omega";
+ prerr_endline "-- NOT IN F_omega";
status, None
(************************ HASKELL *************************)
-let pp_ref status = NCicPp.r2s status false
+(*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
+ `FunctionName
+
+let capitalize classification name =
+ match classification with
+ `Constructor
+ | `TypeName -> String.capitalize name
+ | `FunctionName -> String.uncapitalize name
+
+let pp_ref status ref =
+ capitalize (classify_reference status ref)
+ (NCicPp.r2s status false ref)
+
+let name_of_uri classification uri =
+ capitalize classification (NUri.name_of_uri uri)
(* cons avoid duplicates *)
let rec (@::) name l =
- if name.[0] = '_' then "a" @:: 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 rec pp_kind =
function
Type -> "*"
let rec pp_typ status ctx =
function
Var n -> List.nth ctx (n-1)
+ | Unit -> "()"
| Top -> assert false (* ??? *)
| TConst ref -> pp_ref status ref
| Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2
| Skip t -> pp_typ status ("_"::ctx) t
- | Forall (name,_,t) -> "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")"
+ | Forall (name,_,t) ->
+ (*CSC: BUG HERE: avoid clashes due to uncapitalisation*)
+ let name = String.uncapitalize name in
+ "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")"
| TAppl tl -> "(" ^ String.concat " " (List.map (pp_typ status ctx) tl) ^ ")"
let rec pp_term status ctx =
function
Rel n -> List.nth ctx (n-1)
+ | UnitTerm -> "()"
| Const ref -> pp_ref status ref
| Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")"
| Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")"
| LetIn (name,s,t) ->
"(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^
")"
- | Match _ -> assert false (* TODO of reference * term * term list *)
+ | Match (r,matched,pl) ->
+ let constructors, leftno =
+ let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in
+ let _,_,_,cl = List.nth tys n in
+ cl,leftno
+ in
+ let rec eat_branch n ty pat =
+ match (ty, pat) with
+ | NCic.Prod (_, _, t), _ when n > 0 ->
+ eat_branch (pred n) t pat
+ | NCic.Prod (_, _, t), Lambda (name, t') ->
+ (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*)
+ let cv, rhs = eat_branch 0 t t' in
+ name :: cv, rhs
+ | _, _ -> [], pat
+ in
+ let j = ref 0 in
+ let patterns =
+ try
+ List.map2
+ (fun (_, name, ty) pat ->
+ incr j;
+ name, eat_branch leftno ty pat
+ ) constructors pl
+ with Invalid_argument _ -> assert false
+ in
+ "case " ^ pp_term status ctx matched ^ " of\n" ^
+ String.concat "\n"
+ (List.map
+ (fun (name,(bound_names,rhs)) ->
+ let pattern,body =
+ (*CSC: BUG avoid name clashes *)
+ String.concat " " (String.capitalize name::bound_names),
+ pp_term status ((List.rev bound_names)@ctx) rhs
+ in
+ " " ^ pattern ^ " -> " ^ body
+ ) patterns)
| TLambda t -> pp_term status ctx t
| Inst t -> pp_term status ctx t
type term_former_decl = term_context * typ
*)
-let pp_obj status (uri,obj_kind) =
- let printctx ctx =
+let rec pp_obj status (uri,obj_kind) =
+ let pp_ctx ctx =
String.concat " " (List.rev
(List.fold_right (fun (x,_) l -> x@::l)
(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
+ (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in
match obj_kind with
TypeDeclaration (ctx,_) ->
- (* data?? unsure semantics *)
- "data " ^ NUri.name_of_uri uri ^ " " ^ printctx ctx
+ (* data?? unsure semantics: inductive type without constructor, but
+ not matchable apparently *)
+ "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx
| TypeDefinition ((ctx,_),ty) ->
let namectx = namectx_of_ctx ctx in
- "type " ^ NUri.name_of_uri uri ^ " " ^ printctx ctx ^ " = " ^
+ "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
pp_typ status namectx ty
| TermDeclaration (ctx,ty) ->
- (*CSC: Ask Dominic about the syntax *)
- let namectx = namectx_of_ctx ctx in
- "let " ^ NUri.name_of_uri uri ^ " " ^ printctx ctx ^
- " : " ^ pp_typ status namectx ty
+ (* Implemented with undefined, the best we can do *)
+ let name = name_of_uri `FunctionName uri in
+ name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^
+ name ^ " = undefined"
| TermDefinition ((ctx,ty),bo) ->
- (*CSC: Ask Dominic about the syntax *)
+ let name = name_of_uri `FunctionName uri in
let namectx = namectx_of_ctx ctx in
- "let " ^ NUri.name_of_uri uri ^ " " ^ printctx ctx ^
- " : " ^ pp_typ status namectx ty ^ " = " ^
- pp_term status namectx bo
- | LetRec _ -> assert false (* TODO
- (* inductive and records missing *)*)
+ (*CSC: BUG here *)
+ name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^
+ name ^ " = " ^ pp_term status namectx bo
+ | LetRec l ->
+ (*CSC: BUG always uses the name of the URI *)
+ String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l)
+ | Algebraic il ->
+ String.concat "\n"
+ (List.map
+ (fun _name,ctx,cl ->
+ (*CSC: BUG always uses the name of the URI *)
+ "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^
+ String.concat " | " (List.map
+ (fun name,tys ->
+ capitalize `Constructor name ^
+ String.concat " " (List.map (pp_typ status []) tys)
+ ) cl
+ )) il)
+ (* inductive and records missing *)
let haskell_of_obj status obj =
let status, obj = obj_of status obj in
- status,HExtlib.map_option (pp_obj status) obj
+ status,
+ match obj with
+ None -> "-- ERASED\n"
+ | Some obj -> pp_obj status obj ^ "\n"
(*
let rec typ_of context =
| C.Appl li ->
"(" ^ String.concat " " (clean_args context li) ^ ")"
| C.Const (uri,exp_named_subst) ->
- qualified_name_of_uri current_module_uri uri ^
+ qualified_name_of_uri status current_module_uri uri ^
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
- qualified_name_of_uri current_module_uri
+ qualified_name_of_uri status current_module_uri
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
- qualified_name_of_uri current_module_uri ~capitalize:true
+ qualified_name_of_uri status current_module_uri ~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
| C.Prod (_,_,bo) -> 1 + count_prods 0 bo
| _ -> 0
in
- qualified_name_of_uri current_module_uri
+ qualified_name_of_uri status current_module_uri
~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
| (_,_) -> raise NotEnoughElements
;;
-let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
+let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri =
let name =
if capitalize then
- String.capitalize (UriManager.name_of_uri uri)
+ String.capitalize (UriManager.name_of_uri status uri)
else
- ppid (UriManager.name_of_uri uri) in
+ ppid (UriManager.name_of_uri status uri) in
let filename =
let suri = UriManager.buri_of_uri uri in
let s = String.sub suri 5 (String.length suri - 5) in
NotEnoughElements -> string_of_int (List.length context - n)
end
| C.Var (uri,exp_named_subst) ->
- qualified_name_of_uri current_module_uri uri ^
+ qualified_name_of_uri status current_module_uri uri ^
pp_exp_named_subst exp_named_subst context
| C.Meta (n,l1) ->
(match metasenv with
| C.Appl li ->
"(" ^ String.concat " " (clean_args context li) ^ ")"
| C.Const (uri,exp_named_subst) ->
- qualified_name_of_uri current_module_uri uri ^
+ qualified_name_of_uri status current_module_uri uri ^
pp_exp_named_subst exp_named_subst context
| C.MutInd (uri,n,exp_named_subst) ->
(try
match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
C.InductiveDefinition (dl,_,_,_) ->
let (name,_,_,_) = get_nth dl (n+1) in
- qualified_name_of_uri current_module_uri
+ qualified_name_of_uri status current_module_uri
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
C.InductiveDefinition (dl,_,_,_) ->
let _,_,_,cons = get_nth dl (n1+1) in
let id,_ = get_nth cons n2 in
- qualified_name_of_uri current_module_uri ~capitalize:true
+ qualified_name_of_uri status current_module_uri ~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^
pp_exp_named_subst exp_named_subst context
| C.Prod (_,_,bo) -> 1 + count_prods 0 bo
| _ -> 0
in
- qualified_name_of_uri current_module_uri
+ qualified_name_of_uri status current_module_uri
~capitalize:true
(UriManager.uri_of_string
(UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")),
"\\subst[" ^
String.concat " ; " (
List.map
- (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
+ (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context)
exp_named_subst
) ^ "]"
and clean_args_for_constr nparams context =