X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=4e167004d0b5e4a41d9dcf22e1792486e0b880f0;hb=9956360248d4d6cda67fb1363de22097ccaed533;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..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 @@ -63,22 +63,29 @@ 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 let rec size_of_type = function - | Var v -> 1 - | Unit -> 1 - | Top -> 1 - | TConst c -> 1 + | Var _ -> 0 + | Unit -> 0 + | Top -> 0 + | TConst _ -> 0 | Arrow _ -> 2 - | Skip t -> size_of_type t + | TSkip t -> size_of_type t | Forall _ -> 2 - | TAppl l -> 1 + | TAppl _ -> 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,84 @@ 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 mk_tappl f l = + match f with + TAppl args -> TAppl (args@l) + | _ -> TAppl (f::l) + let rec size_of_term = function - | Rel r -> 1 + | Rel _ -> 1 | UnitTerm -> 1 - | Const c -> 1 - | Lambda (name, body) -> 1 + size_of_term body + | Const _ -> 1 + | 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 +module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) -type typ_former_decl = typ_context * kind -type typ_former_def = typ_former_decl * typ +module GlobalNames = Set.Make(String) -type term_former_decl = term_context * typ -type term_former_def = term_former_decl * term +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 * GlobalNames.t + +let empty_info = [] 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 (info * NReference.reference * obj_kind) list + (* reference, left, right, constructors *) + | Algebraic of (info * NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list + +type obj = info * NReference.reference * obj_kind + +(* For LetRec and Algebraic blocks *) +let dummyref = + NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" + +type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];; -type obj = NUri.uri * obj_kind +let max_not_term t1 t2 = + match t1,t2 with + `KindOrType,_ + | _,`KindOrType -> `KindOrType + | `Kind,_ + | _,`Kind -> `Kind + | `Type,_ + | _,`Type -> `Type + | `PropKind,_ + | _,`PropKind -> `PropKind + | `Proposition,`Proposition -> `Proposition + +let sup = List.fold_left max_not_term `Proposition let rec classify_not_term status context t = match NCicReduction.whd status ~subst:[] context t with @@ -139,14 +185,23 @@ let rec classify_not_term status context t = classify_not_term status ((b,NCic.Decl s)::context) t | NCic.Implicit _ | NCic.LetIn _ - | NCic.Lambda _ | NCic.Const (NReference.Ref (_,NReference.CoFix _)) - | NCic.Appl [] -> assert false (* NOT POSSIBLE *) - | NCic.Match _ + | NCic.Appl [] -> + assert false (* NOT POSSIBLE *) + | NCic.Lambda (n,s,t) -> + (* Lambdas can me met in branches of matches, expecially when the + output type is a product *) + classify_not_term status ((n,NCic.Decl s)::context) t + | NCic.Match (_,_,_,pl) -> + let classified_pl = List.map (classify_not_term status context) pl in + sup classified_pl | NCic.Const (NReference.Ref (_,NReference.Fix _)) -> - (* be aware: we can be the head of an application *) - assert false (* TODO *) + assert false (* IMPOSSIBLE *) | NCic.Meta _ -> assert false (* TODO *) + | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix (i,_,_)) as r)::_)-> + let l,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes status r in + let _,_,_,_,bo = List.nth l i in + classify_not_term status [] bo | NCic.Appl (he::_) -> classify_not_term status context he | NCic.Rel n -> let rec find_sort typ = @@ -190,8 +245,6 @@ let rec classify_not_term status context t = assert false (* IMPOSSIBLE *) ;; -type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];; - let classify status ~metasenv context t = match NCicTypeChecker.typeof status ~metasenv ~subst:[] context t with | NCic.Sort _ -> @@ -251,10 +304,6 @@ let rec skip_args status ~metasenv context = | `Term _ -> assert false (* IMPOSSIBLE *) ;; -module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) - -type db = (typ_context * typ option) ReferenceMap.t - class type g_status = object method extraction_db: db @@ -263,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 @@ -271,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 @@ -282,7 +345,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 +354,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 = @@ -312,15 +375,26 @@ let rec split_typ_lambdas status n ~metasenv context typ = ;; -let context_of_typformer status ~metasenv context = +let rev_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.Fix _) as ref) -> - (try 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 -> assert false (* IMPOSSIBLE *)) + 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 *) + let rec dummy = None::dummy in + dummy) | NCic.Match _ -> assert false (* TODO ???? *) | NCic.Rel n -> let typ = @@ -329,7 +403,7 @@ let context_of_typformer status ~metasenv context = | _,NCic.Def _ -> assert false (* IMPOSSIBLE *) in let typ_ctx = snd (HExtlib.split_nth n context) in let typ = kind_of status ~metasenv typ_ctx typ in - fst (split_kind_prods [] typ) + List.rev (fst (split_kind_prods [] typ)) | NCic.Meta _ -> assert false (* TODO *) | NCic.Const (NReference.Ref (_,NReference.Con _)) | NCic.Const (NReference.Ref (_,NReference.CoFix _)) @@ -351,41 +425,103 @@ 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 _ | 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 (_,_,_,_) + | NCic.Appl (NCic.Const (NReference.Ref (_,NReference.Fix _))::_) -> + Top | NCic.Appl (he::args) -> - let he_context = context_of_typformer status ~metasenv context he in + let rev_he_context= rev_context_of_typformer status ~metasenv context he in TAppl (typ_of status ~metasenv context he :: List.map (function None -> Unit | Some ty -> typ_of status ~metasenv context ty) - (skip_args status ~metasenv context (List.rev he_context,args))) + (skip_args status ~metasenv context (rev_he_context,args))) | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; otherwise NOT A TYPE *) - | NCic.Meta _ - | NCic.Match (_,_,_,_) -> assert false (* TODO *) + | NCic.Meta _ -> assert false (*TODO*) +;; + +let rec fomega_lift_type_from n k = + function + | Var m as t -> if m < k then t else Var (m + n) + | Top -> Top + | TConst _ as t -> t + | Unit -> Unit + | Arrow (ty1,ty2) -> Arrow (fomega_lift_type_from n k ty1,fomega_lift_type_from n (k+1) ty2) + | TSkip t -> TSkip (fomega_lift_type_from n (k+1) t) + | Forall (name,kind,t) -> Forall (name,kind,fomega_lift_type_from n (k+1) t) + | TAppl args -> TAppl (List.map (fomega_lift_type_from n k) args) + +let fomega_lift_type n t = + if n = 0 then t else fomega_lift_type_from n 0 t + +let fomega_lift_term n t = + let rec fomega_lift_term n k = + function + | Rel m as t -> if m < k then t else Rel (m + n) + | BottomElim + | UnitTerm + | Const _ as t -> t + | Lambda (name,t) -> Lambda (name,fomega_lift_term n (k+1) t) + | TLambda (name,t) -> TLambda (name,fomega_lift_term n (k+1) t) + | Appl args -> Appl (List.map (fomega_lift_term n k) args) + | LetIn (name,m,bo) -> + LetIn (name, fomega_lift_term n k m, fomega_lift_term n (k+1) bo) + | Match (ref,t,pl) -> + let lift_p (ctx,t) = + let lift_context ctx = + let len = List.length ctx in + HExtlib.list_mapi + (fun el i -> + let j = len - i - 1 in + match el with + None + | Some (_,`OfKind _) as el -> el + | Some (name,`OfType t) -> + Some (name,`OfType (fomega_lift_type_from n (k+j) t)) + ) ctx + in + lift_context ctx, fomega_lift_term n (k + List.length ctx) t + in + Match (ref,fomega_lift_term n k t,List.map lift_p pl) + | Inst t -> Inst (fomega_lift_term n k t) + | Skip t -> Skip (fomega_lift_term n (k+1) t) + | UnsafeCoerce t -> UnsafeCoerce (fomega_lift_term n k t) + in + if n = 0 then t else fomega_lift_term n 0 t ;; let rec fomega_subst k t1 = function | Var n -> - if k=n then t1 + if k=n then fomega_lift_type (k-1) 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) + | 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 @@ -399,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 _ @@ -408,14 +616,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 @@ -437,51 +645,148 @@ 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 - (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)) -*) + 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) -> - Match (ref,term_of status ~metasenv context t, - List.map (term_of status ~metasenv context) pl) + let patterns_of pl = + let _,leftno,_,_,_ = NCicEnvironment.get_checked_indtys status ref 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 (* IMPOSSIBLE *) + | TSkip _, _ + | Forall _,_ + | Arrow _,_ -> assert false (*BUG here, eta-expand!*) + | _, _ -> context,ctx, pat + in + try + 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 + ) 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] -> fomega_lift_term (- List.length lhs) rhs + | _ -> 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 = + 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 + | `PropKind + | `Proposition + | `Term `TypeFormer + | `Term `PropFormer + | `Term `Proof + | `Type + | `KindOrType + | `Kind -> UnitTerm + | `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) -> - eat_args status metasenv (Inst acc) - context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl - | Skip 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 + | `Kind -> + eat_args status metasenv (UnsafeCoerce (Inst acc)) + context (fomega_subst 1 Unit t) tl + | `KindOrType + | `Term `TypeFormer + | `Type -> + eat_args status metasenv (Inst acc) + context (fomega_subst 1 (typ_of status ~metasenv context arg) t) + tl + | `Term _ -> assert false (*TODO: ????*)) + | 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 +797,36 @@ type 'a result = | Success of 'a ;; -let object_of_constant status ~metasenv uri height bo ty = +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 -> let ty = kind_of status ~metasenv [] ty in @@ -510,14 +844,10 @@ 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)) + 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 @@ -526,17 +856,19 @@ let object_of_constant status ~metasenv uri height 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 (uri, 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 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 +877,75 @@ 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) -> + 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 - name,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,(name,ctx,cl)::res + status,i+1,(info::infos,ref,left,right,List.rev cl_rev)::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) + 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 (uri, 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,_) -> - 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 (info,ref,obj) -> i+1,status, (info,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 @@ -643,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) @@ -653,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 = @@ -684,28 +1033,34 @@ 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 - `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 = 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) + (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 = @@ -723,88 +1078,103 @@ let rec pretty_print_type status ctxt = function | Var n -> List.nth ctxt (n-1) | Unit -> "()" - | Top -> assert false (* ??? *) + | Top -> "GHC.Prim.Any" | TConst ref -> pp_ref status ref | 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 - | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) + "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t + | 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 = + List.fold_right + (fun el (ctx1,rev_res) -> + match el with + None -> ""@::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 + ) 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) ^ "}\n " + | 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 -*) +xdo_pretty_print_term := pretty_print_term;; -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,48 +1184,87 @@ 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) + ) cl) (*^ "\n deriving (Prelude.Show)"*) + ) il) (* inductive and records missing *) +let rec infos_of (info,_,obj_kind) = + info @ + match obj_kind with + LetRec l -> List.concat (List.map (fun (infos,_,_) -> infos) l) + | Algebraic l -> List.concat (List.map (fun (infos,_,_,_,_) -> infos) l) + | _ -> [] + let haskell_of_obj status (uri,_,_,_,_ as obj) = let status, obj = object_of status obj in status, match obj with - Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n" - | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n" - | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n" - | Success o -> pp_obj status o ^ "\n" + Erased -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to term being propositionally irrelevant.\n",[] + | OutsideTheory -> "-- [?] " ^ NUri.name_of_uri uri ^ " erased due to image of term under extraction residing outside Fω.\n",[] + | Failure msg -> "-- [?] " ^ NUri.name_of_uri uri ^ " FAILURE: " ^ msg ^ "\n",[] + | Success o -> pp_obj status o ^ "\n", infos_of o + +let refresh_uri_in_typ ~refresh_uri_in_reference = + let rec refresh_uri_in_typ = + function + | Var _ + | Unit + | Top as t -> t + | TConst r -> TConst (refresh_uri_in_reference r) + | Arrow (t1,t2) -> Arrow (refresh_uri_in_typ t1, refresh_uri_in_typ t2) + | TSkip t -> TSkip (refresh_uri_in_typ t) + | Forall (n,k,t) -> Forall (n,k,refresh_uri_in_typ t) + | TAppl tl -> TAppl (List.map refresh_uri_in_typ tl) + in + refresh_uri_in_typ + +let refresh_uri_in_info ~refresh_uri_in_reference infos = + List.map + (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