X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=8b8a7b216c74e360238b183789ed2acdb3319c6c;hb=0b2cf1b25d45ffb80b27416e057a58e3dc3f257d;hp=ffc9766b739a72201ffe24f07ba373e2389d7d3f;hpb=4999662218e409f0a5d26515dc0f63928c607426;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index ffc9766b7..8b8a7b216 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -38,6 +38,7 @@ type kind = type typ = Var of int + | Unit | Top | TConst of typformerreference | Arrow of typ * typ @@ -47,6 +48,7 @@ type typ = type term = Rel of int + | UnitTerm | Const of reference | Lambda of string * (* typ **) term | Appl of term list @@ -73,8 +75,8 @@ type obj_kind = | 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 @@ -106,14 +108,33 @@ let rec classify_not_term status no_dep_prods context t = 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 @@ -126,7 +147,7 @@ let rec classify_not_term status no_dep_prods context t = | `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];; @@ -137,7 +158,6 @@ let classify status ~metasenv context t = (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 @@ -150,7 +170,8 @@ prerr_endline ("XXX: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty); 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 @@ -183,16 +204,17 @@ let rec skip_args status ~metasenv context = 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 @@ -225,6 +247,14 @@ let rec split_typ_prods context = | _ 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 @@ -247,9 +277,9 @@ let 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.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 ???? *) @@ -293,7 +323,8 @@ let rec typ_of status ~metasenv context k = | 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 *) @@ -301,6 +332,34 @@ let rec typ_of status ~metasenv context k = | 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 _ @@ -321,6 +380,7 @@ let rec term_of status ~metasenv context = | `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) @@ -331,22 +391,121 @@ let rec term_of status ~metasenv context = | `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) = @@ -360,62 +519,69 @@ 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 -> "*" @@ -425,23 +591,64 @@ let rec pp_kind = 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 @@ -452,39 +659,57 @@ type term_former_def = term_context * term * typ 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 = @@ -585,14 +810,14 @@ 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 @@ -607,7 +832,7 @@ let rec typ_of 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 @@ -657,7 +882,7 @@ let rec typ_of 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")), @@ -828,12 +1053,12 @@ let rec get_nth l n = | (_,_) -> 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 @@ -873,7 +1098,7 @@ let rec pp ~in_type t context = 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 @@ -964,14 +1189,14 @@ let rec pp ~in_type t 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 @@ -986,7 +1211,7 @@ let rec pp ~in_type t 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 @@ -1036,7 +1261,7 @@ let rec pp ~in_type t 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")), @@ -1138,7 +1363,7 @@ and pp_exp_named_subst exp_named_subst context = "\\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 =