X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=6b797ef449beb26978929f8a5ed113b57e695c99;hb=c2a0823b4837cfe8ca7f89e68f58cd97efacf367;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..6b797ef44 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -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 + | Var _ -> 1 | Unit -> 1 | Top -> 1 - | TConst c -> 1 + | TConst _ -> 1 | 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,80 @@ 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 + | 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 +type info_el = typ_context * typ option +type info = (NReference.reference * info_el) list +type db = info_el ReferenceMap.t -type term_former_decl = term_context * typ -type term_former_def = term_former_decl * term +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 | 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];; + +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 -type obj = NUri.uri * obj_kind +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 +181,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 +241,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 +300,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 @@ -282,7 +327,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 +336,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 +357,21 @@ 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 List.rev (fst (ReferenceMap.find ref status#extraction_db)) 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 +380,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,7 +402,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 _ @@ -359,29 +410,81 @@ let rec typ_of status ~metasenv context k = | NCic.Lambda _ -> 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 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) @@ -408,14 +511,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 +542,77 @@ 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 (* IMPOSSIBLE *) + | TSkip _, _ + | Forall _,_ + | Arrow _,_ -> assert false (*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] -> 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 = @@ -476,12 +620,39 @@ and eat_args status metasenv acc context tyhe = Unit -> UnitTerm | _ -> term_of status ~metasenv context arg in eat_args status metasenv (mk_appl acc arg) context 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 + 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 -> + (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 + | `Type -> + eat_args status metasenv (Inst acc) + context (fomega_subst 1 (typ_of status ~metasenv context arg) t) + tl) + | 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 +663,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 +681,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 + let info = ref,(nicectx,Some bo) in status#set_extraction_db - (ReferenceMap.add ref (nicectx,Some bo) - status#extraction_db), - Success (uri,TypeDefinition((nicectx,res),bo)) + (register_info status#extraction_db info), + Success ([info],ref,TypeDefinition((nicectx,res),bo)) | `Kind -> status, Erased (* DPM: but not really, more a failure! *) | `PropKind | `Proposition -> status, Erased @@ -529,14 +697,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 +713,71 @@ 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 +prerr_endline ("AGGIUNGO" ^ NReference.string_of_reference ref); + let info = ref,(ctx,None) in let status = status#set_extraction_db - (ReferenceMap.add ref (ctx,None) status#extraction_db) in + (register_info status#extraction_db info) 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,([info],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 + let info = ref,(ctx,None) in status#set_extraction_db - (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res) + (register_info status#extraction_db info), + 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)) + 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 (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 @@ -690,22 +871,25 @@ let classify_reference status ref = if ReferenceMap.mem ref status#extraction_db then `TypeName else - `FunctionName + let NReference.Ref (_,r) = ref in + match r 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 = @@ -723,88 +907,90 @@ let rec pretty_print_type status ctxt = function | Var n -> List.nth ctxt (n-1) | Unit -> "()" - | Top -> assert false (* ??? *) + | Top -> "Top" | 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 + "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,48 +1000,79 @@ 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) (* 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,(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)) + infos