X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=4e167004d0b5e4a41d9dcf22e1792486e0b880f0;hb=9956360248d4d6cda67fb1363de22097ccaed533;hp=ea38f82dc7dc7a6f104091ce9d59458ddaf8ee90;hpb=ce0ddf1d4782a7cc2647adecb1b92d0e2b9c37eb;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index ea38f82dc..4e167004d 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -43,8 +43,8 @@ let rec size_of_kind = | 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 @@ -69,10 +69,10 @@ type typ = 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 @@ -109,6 +109,11 @@ let mk_appl f x = 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 @@ -127,16 +132,15 @@ let rec size_of_term = 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 of typ | `Function of typ ] 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 @@ -308,7 +312,7 @@ class type g_status = 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 @@ -316,6 +320,20 @@ class virtual status = = 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 @@ -363,13 +381,18 @@ let rev_context_of_typformer status ~metasenv context = | 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 ???? *) @@ -407,7 +430,7 @@ let rec typ_of status ~metasenv context k = | NCic.Sort _ | NCic.Implicit _ | NCic.LetIn _ -> assert false (* IMPOSSIBLE *) - | NCic.Lambda _ -> assert false (* LAMBDA-LIFT INNER DECLARATION *) + | NCic.Lambda _ -> Top (*assert false (* LAMBDA-LIFT INNER DECLARATION *)*) | NCic.Rel n -> Var n | NCic.Const ref -> TConst ref | NCic.Match (_,_,_,_) @@ -477,7 +500,7 @@ let fomega_lift_term n t = let rec fomega_subst k t1 = function | Var n -> - if k=n then fomega_lift_type k t1 + if k=n then fomega_lift_type (k-1) t1 else if n < k then Var n else Var (n-1) | Top -> Top @@ -486,9 +509,19 @@ let rec fomega_subst k t1 = | 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 args -> TAppl (List.map (fomega_subst k t1) args) - -let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db) + | 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 @@ -502,6 +535,78 @@ let rec fomega_whd status 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 _ @@ -540,22 +645,15 @@ let rec term_of status ~metasenv context = | NCic.Rel n -> Rel n | NCic.Const ref -> Const ref | 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 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 constructors, leftno = - let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in - let _,_,_,cl = List.nth tys n in - cl,leftno - in + let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref in let rec eat_branch n ty context ctx pat = match (ty, pat) with | TSkip t,_ @@ -585,17 +683,26 @@ let rec term_of status ~metasenv context = | _, _ -> 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 + 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 - ) constructors pl + ) pl with Invalid_argument _ -> assert false in (match classify_not_term status [] (NCic.Const ref) with @@ -615,11 +722,29 @@ and eat_args status metasenv acc context tyhe = | arg::tl -> match fomega_whd status tyhe with Arrow (s,t) -> - let arg = + let acc = match s with - Unit -> UnitTerm - | _ -> term_of status ~metasenv context arg in - eat_args status metasenv (mk_appl acc arg) context t tl + 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 @@ -634,23 +759,32 @@ and eat_args status metasenv acc context tyhe = | `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 - | `Term `TypeFormer | `Kind -> eat_args status metasenv (UnsafeCoerce (Inst acc)) context (fomega_subst 1 Unit t) tl - | `Term _ -> assert false (*TODO: ????*) | `KindOrType + | `Term `TypeFormer | `Type -> eat_args status metasenv (Inst acc) context (fomega_subst 1 (typ_of status ~metasenv context arg) t) - tl) + tl + | `Term _ -> assert false (*TODO: ????*)) | TSkip t -> eat_args status metasenv acc context t tl | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *) @@ -663,6 +797,35 @@ type 'a result = | 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 -> @@ -682,10 +845,9 @@ let object_of_constant status ~metasenv ref bo ty = 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 @@ -694,10 +856,12 @@ let object_of_constant status ~metasenv ref bo ty = | `Proposition -> status, Erased | `KindOrType (* ??? *) | `Type -> - (* CSC: TO BE FINISHED, REF NON REGISTERED *) 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 ([],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." ;; @@ -716,20 +880,23 @@ let object_of_inductive status ~metasenv uri ind leftno il = 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 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],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 @@ -746,16 +913,18 @@ let object_of status (uri,height,metasenv,subst,obj_kind) = | `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 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 @@ -823,7 +992,7 @@ let string_of_char_list s = * ---------------------------------------------------------------------------- *) -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) @@ -833,7 +1002,7 @@ let remove_underscores_and_mark = 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 = @@ -864,17 +1033,15 @@ let idiomatic_haskell_term_name_of_string = 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 = @@ -888,7 +1055,12 @@ 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 = @@ -906,7 +1078,7 @@ let rec pretty_print_type status ctxt = 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 ^ " -> " ^ @@ -920,7 +1092,15 @@ let rec pretty_print_type status ctxt = "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) +;; + +xdo_pretty_print_type := pretty_print_type;; + let pretty_print_term_context status ctx1 ctx2 = let name_context, rev_res = @@ -928,8 +1108,11 @@ let pretty_print_term_context status ctx1 ctx2 = (fun el (ctx1,rev_res) -> match el with None -> ""@::ctx1,rev_res - | Some (name,`OfKind _) -> name@::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 @@ -979,6 +1162,8 @@ let rec pretty_print_term status ctxt = | 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 @@ -1031,8 +1216,8 @@ let rec pp_obj status (_,ref,obj_kind) = let namectx = namectx_of_ctx left in pp_ref status ref ^ " :: " ^ pretty_print_type status namectx tys - ) cl - )) il) + ) cl) (*^ "\n deriving (Prelude.Show)"*) + ) il) (* inductive and records missing *) let rec infos_of (info,_,obj_kind) = @@ -1067,11 +1252,19 @@ let refresh_uri_in_typ ~refresh_uri_in_reference = 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 + 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