X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=7b24f74c0c741b799f29dd6d95f7318bd1eac82f;hb=87e64004d2fb44077b68c4f9c009223b81ad2b6d;hp=4f3892cbc992f9e6738136f05163254ab3283404;hpb=ceac1e90a8108f526e33bbae7173571c55ea802d;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 4f3892cbc..7b24f74c0 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -63,7 +63,7 @@ type typ = | Top | TConst of typformerreference | Arrow of typ * typ - | Skip of typ + | TSkip of typ | Forall of string * kind * typ | TAppl of typ list @@ -74,11 +74,18 @@ let rec size_of_type = | Top -> 1 | TConst c -> 1 | Arrow _ -> 2 - | Skip t -> size_of_type t + | TSkip t -> size_of_type t | Forall _ -> 2 | TAppl l -> 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 @@ -86,45 +93,54 @@ type term = | Lambda of string * (* typ **) term | Appl of term list | LetIn of string * (* typ **) term * term - | Match of reference * term * term list - | TLambda of (* string **) 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 rec size_of_term = function | Rel r -> 1 | UnitTerm -> 1 | Const c -> 1 - | Lambda (name, body) -> 1 + size_of_term body + | Lambda (_, body) -> 1 + size_of_term body | Appl l -> List.length l - | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body - | Match (name, case, pats) -> 1 + size_of_term case + List.length pats - | TLambda t -> size_of_term t + | 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 ;; let unitty = NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));; -(* 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_former_decl = term_context * typ -type term_former_def = term_former_decl * term - 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 obj_kind list - | Algebraic of (string * typ_context * (string * typ) list) list + | LetRec of (NReference.reference * obj_kind) list + (* reference, left, right, constructors *) + | Algebraic of (NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list -type obj = NUri.uri * obj_kind +type obj = NReference.reference * obj_kind + +(* For LetRec and Algebraic blocks *) +let dummyref = + NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" let rec classify_not_term status context t = match NCicReduction.whd status ~subst:[] context t with @@ -282,7 +298,7 @@ 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 - | Skip ta -> split_typ_prods (None::context) ta + | TSkip ta -> split_typ_prods (None::context) ta | _ as t -> context,t ;; @@ -291,7 +307,7 @@ let rec glue_ctx_typ ctx typ = | [] -> 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) + | None::ctx -> glue_ctx_typ ctx (TSkip typ) ;; let rec split_typ_lambdas status n ~metasenv context typ = @@ -320,7 +336,9 @@ let context_of_typformer status ~metasenv context = | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) -> (try fst (ReferenceMap.find ref status#extraction_db) with - Not_found -> assert false (* IMPOSSIBLE *)) + Not_found -> + prerr_endline ("REF NOT FOUND: " ^ NReference.string_of_reference ref); + assert false (* IMPOSSIBLE *)) | NCic.Match _ -> assert false (* TODO ???? *) | NCic.Rel n -> let typ = @@ -351,7 +369,7 @@ let rec typ_of status ~metasenv context k = typ_of status ~metasenv ((b,NCic.Decl s)::context) t) | `PropKind | `Proposition -> - Skip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t) + TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t) | `Term _ -> assert false (* IMPOSSIBLE *)) | NCic.Sort _ | NCic.Implicit _ @@ -381,7 +399,7 @@ let rec fomega_subst k t1 = | 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) + | TSkip t -> TSkip (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) @@ -408,14 +426,14 @@ let rec term_of status ~metasenv context = (* CSC: non-invariant assumed here about "_" *) (match classify status ~metasenv context ty with | `Kind -> - TLambda (term_of status ~metasenv ((b,NCic.Decl ty)::context) bo) + 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 ??? *) - term_of status ~metasenv ((b,NCic.Decl ty)::context) bo + 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 @@ -439,36 +457,75 @@ let rec term_of status ~metasenv context = | NCic.Appl (he::args) -> eat_args status metasenv (term_of status ~metasenv context he) context + (*BUG: recomputing every time the type of the head*) (typ_of status ~metasenv context (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he)) args -(* - let he_context = context_of_typformer status ~metasenv context he in - 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) + let patterns_of pl = + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in + let _,_,_,cl = List.nth tys n in + cl,leftno + 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 (*TODO: HOW??*) + (*BUG here, eta-expand!*) + | _, _ -> context,ctx, pat + in + try + List.map2 + (fun (_, name, ty) pat -> + (*BUG: recomputing every time the type of the constructor*) + let ty = typ_of status ~metasenv context ty 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 + ) constructors 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] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*) + | _ -> 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 -> - 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 = @@ -479,7 +536,7 @@ and eat_args status metasenv acc context tyhe = | Forall (_,_,t) -> eat_args status metasenv (Inst acc) context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl - | Skip t -> + | TSkip t -> eat_args status metasenv acc context t tl | Top -> assert false (*TODO: HOW??*) | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *) @@ -492,7 +549,7 @@ type 'a result = | Success of 'a ;; -let object_of_constant status ~metasenv uri height bo ty = +let object_of_constant status ~metasenv ref bo ty = match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in @@ -510,14 +567,11 @@ let object_of_constant status ~metasenv uri height bo ty = 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), - Success (uri,TypeDefinition((nicectx,res),bo)) + Success (ref,TypeDefinition((nicectx,res),bo)) | `Kind -> status, Erased (* DPM: but not really, more a failure! *) | `PropKind | `Proposition -> status, Erased @@ -529,14 +583,14 @@ let object_of_constant status ~metasenv uri height bo ty = (* CSC: TO BE FINISHED, REF NON REGISTERED *) let ty = typ_of status ~metasenv [] ty in status, - Success (uri, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo)) + Success (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) (_,name,arity,cl) -> + (fun (status,i,res) (_,_,arity,cl) -> match classify_not_term status [] arity with | `Proposition | `KindOrType @@ -545,58 +599,68 @@ let object_of_inductive status ~metasenv uri ind leftno il = | `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 status = status#set_extraction_db (ReferenceMap.add ref (ctx,None) status#extraction_db) in let cl = - List.map - (fun (_,name,ty) -> + HExtlib.list_mapi + (fun (_,_,ty) j -> let ctx,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in let ty = typ_of status ~metasenv ctx ty in - name,ty + NReference.mk_constructor (j+1) ref,ty ) cl in - status,i+1,(name,ctx,cl)::res + status,i+1,(ref,left,right,cl)::res ) (status,0,[]) il in match rev_tyl with [] -> status,Erased - | _ -> status, Success (uri, Algebraic (List.rev rev_tyl)) + | _ -> 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 ref = NReference.reference_of_spec uri NReference.Decl in status#set_extraction_db - (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res) + (ReferenceMap.add ref (ctx,None) status#extraction_db), + Success (ref, TypeDeclaration res) | `PropKind | `Proposition -> status, Erased | `Type | `KindOrType (*???*) -> let ty = typ_of status ~metasenv [] ty in - status, Success (uri, TermDeclaration (split_typ_prods [] ty)) + status, Success (ref, TermDeclaration (split_typ_prods [] ty)) | `Term _ -> status, Failure "Type classified as a term. This is a bug.") | NCic.Constant (_,_,Some bo,ty,_) -> - object_of_constant status ~metasenv uri height bo ty - | NCic.Fixpoint (_fix_or_cofix,fs,_) -> - let status,objs = + 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,_,ty,bo) (status,res) -> - let status,obj = object_of_constant ~metasenv status uri height bo ty in + (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 (_uri,obj) -> status, obj::res - | _ -> status, res) fs (status,[]) + | Success (ref,obj) -> i+1,status, (ref,obj)::res + | _ -> i+1,status, res) fs (0,status,[]) in - status, Success (uri,LetRec objs) + status, Success (dummyref,LetRec objs) | NCic.Inductive (ind,leftno,il,_) -> object_of_inductive status ~metasenv uri ind leftno il @@ -690,22 +754,25 @@ let classify_reference status ref = if ReferenceMap.mem ref status#extraction_db then `TypeName else - `FunctionName + let NReference.Ref (_,ref) = ref in + match ref with + NReference.Con _ -> `Constructor + | NReference.Ind _ -> assert false + | _ -> `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) - (NCicPp.r2s status false ref) - -let name_of_uri classification uri = - capitalize classification (NUri.name_of_uri uri) + (NCicPp.r2s status true ref) (* cons avoid duplicates *) let rec (@:::) name l = @@ -728,83 +795,85 @@ let rec pretty_print_type status ctxt = | Arrow (t1,t2) -> bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^ pretty_print_type status ("_"::ctxt) t2 - | Skip t -> pretty_print_type status ("_"::ctxt) t + | TSkip t -> pretty_print_type status ("_"::ctxt) t | Forall (name, kind, t) -> (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) - let name = String.uncapitalize name in + 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 + "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t else - "forall " ^ name ^ ". " ^ pretty_print_type status (name@::ctxt) t + "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) +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 _) -> name@::ctx1,rev_res + | Some (name,`OfType typ) -> + 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) -> "\\" ^ name ^ " -> " ^ pretty_print_term status (name@::ctxt) t + | 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 ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) 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 - 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 " ^ pretty_print_term status ctxt 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), - pretty_print_term status ((List.rev bound_names)@ctxt) rhs - in - " " ^ pattern ^ " -> " ^ body - ) patterns) - | TLambda t -> pretty_print_term status ctxt t + "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) + | 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 ;; -(* -type term_context = (string * [`OfKind of kind | `OfType of typ]) option list - -type term_former_def = term_context * term * typ -type term_former_decl = term_context * typ -*) - -let rec pp_obj status (uri,obj_kind) = +let rec pp_obj status (ref,obj_kind) = let pretty_print_context ctx = - String.concat " " (List.rev + String.concat " " (List.rev (snd (List.fold_right - (fun (x,kind) l -> + (fun (x,kind) (l,res) -> let x,l = x @:::l in if size_of_kind kind > 1 then - ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l + x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res else - x::l) - (HExtlib.filter_map (fun x -> x) ctx) [])) + x::l,x::res) + (HExtlib.filter_map (fun x -> x) ctx) ([],[])))) in let namectx_of_ctx ctx = List.fold_right (@::) @@ -814,38 +883,37 @@ let rec pp_obj status (uri,obj_kind) = (* data?? unsure semantics: inductive type without constructor, but not matchable apparently *) if List.length ctx = 0 then - "data " ^ name_of_uri `TypeName uri + "data " ^ pp_ref status ref else - "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx + "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 " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty + "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty else - "type " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty + "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty | TermDeclaration (ctx,ty) -> - let name = name_of_uri `FunctionName uri in + 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 = name_of_uri `FunctionName uri in + 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 -> - (*CSC: BUG always uses the name of the URI *) - String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l) + String.concat "\n" (List.map (pp_obj status) 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 ^ " " ^ pretty_print_context ctx ^ " where\n " ^ + (fun ref,left,right,cl -> + "data " ^ pp_ref status ref ^ " " ^ + pretty_print_context (right@left) ^ " where\n " ^ String.concat "\n " (List.map - (fun name,tys -> - let namectx = namectx_of_ctx ctx in - capitalize `Constructor name ^ " :: " ^ + (fun ref,tys -> + let namectx = namectx_of_ctx left in + pp_ref status ref ^ " :: " ^ pretty_print_type status namectx tys ) cl )) il)