X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=6b797ef449beb26978929f8a5ed113b57e695c99;hb=c2a0823b4837cfe8ca7f89e68f58cd97efacf367;hp=76b53f363658f46a42e70898ead686a989001787;hpb=c742f5b1450507df01cb0379d85b4170ddf6cad5;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 76b53f363..6b797ef44 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -32,33 +32,52 @@ type typformerreference = NReference.reference type reference = NReference.reference type kind = - Type - | KArrow of kind * kind - | KSkip of kind (* dropped abstraction *) + | Type + | KArrow of kind * kind + | KSkip of kind (* dropped abstraction *) -type typ = - Var of int - | Unit - | Top - | TConst of typformerreference - | Arrow of typ * typ - | Skip of typ - | Forall of string * kind * typ - | TAppl of typ list +let rec size_of_kind = + function + | Type -> 1 + | KArrow (l, r) -> 1 + size_of_kind l + size_of_kind r + | KSkip k -> size_of_kind k +;; -type term = - Rel of int - | UnitTerm - | Const of reference - | 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 - | Inst of (*typ_former **) term - -let unitty = - NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));; +let bracket size_of pp o = + if size_of o > 1 then + "(" ^ pp o ^ ")" + else + pp o +;; + +let rec pretty_print_kind = + function + | Type -> "*" + | KArrow (l, r) -> bracket size_of_kind pretty_print_kind l ^ " -> " ^ pretty_print_kind r + | KSkip k -> pretty_print_kind k +;; + +type typ = + | Var of int + | Unit + | Top + | TConst of typformerreference + | Arrow of typ * typ + | TSkip of typ + | Forall of string * kind * typ + | TAppl of typ list + +let rec size_of_type = + function + | Var _ -> 1 + | Unit -> 1 + | Top -> 1 + | TConst _ -> 1 + | Arrow _ -> 2 + | TSkip t -> size_of_type t + | Forall _ -> 2 + | TAppl _ -> 1 +;; (* None = dropped abstraction *) type typ_context = (string * kind) option list @@ -67,47 +86,119 @@ 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 + | Const of reference + | Lambda of string * (* typ **) term + | Appl of term list + | LetIn of string * (* typ **) term * 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 _ -> 1 + | UnitTerm -> 1 + | Const _ -> 1 + | Lambda (_, body) -> 1 + size_of_term body + | Appl l -> List.length l + | 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 +;; + +module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) + +type info_el = typ_context * typ option +type info = (NReference.reference * info_el) list +type db = info_el ReferenceMap.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 | TermDeclaration of term_former_decl | TermDefinition of term_former_def - | LetRec of obj_kind list - (* inductive and records missing *) + | 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 -type obj = NUri.uri * obj_kind +(* For LetRec and Algebraic blocks *) +let dummyref = + NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" -exception NotInFOmega +type not_term = [`Kind | `KindOrType | `PropKind | `Proposition | `Type];; -let rec classify_not_term status no_dep_prods context t = +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 | NCic.Sort s -> (match s with NCic.Prop | NCic.Type [`CProp,_] -> `PropKind - | NCic.Type [`Type,_] -> - if no_dep_prods then `Kind - else - raise NotInFOmega (* ?? *) + | NCic.Type [`Type,_] -> `Kind | NCic.Type _ -> assert false) | NCic.Prod (b,s,t) -> (*CSC: using invariant on "_" *) - classify_not_term status (no_dep_prods && b.[0] = '_') - ((b,NCic.Decl s)::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 (he::_) -> classify_not_term status no_dep_prods context he + | 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 = match NCicReduction.whd status ~subst:[] context (NCicSubstitution.lift status n typ) with @@ -130,7 +221,7 @@ let rec classify_not_term status no_dep_prods context t = | _,NCic.Def _ -> assert false (* IMPOSSIBLE *)) | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) -> let _,_,ty,_,_ = NCicEnvironment.get_checked_decl status ref in - (match classify_not_term status true [] ty with + (match classify_not_term status [] ty with | `Proposition | `Type -> assert false (* IMPOSSIBLE *) | `Kind @@ -139,7 +230,7 @@ let rec classify_not_term status no_dep_prods context t = | NCic.Const (NReference.Ref (_,NReference.Ind _) as ref) -> let _,_,ityl,_,i = NCicEnvironment.get_checked_indtys status ref in let _,_,arity,_ = List.nth ityl i in - (match classify_not_term status true [] arity with + (match classify_not_term status [] arity with | `Proposition | `Type | `KindOrType -> assert false (* IMPOSSIBLE *) @@ -150,16 +241,14 @@ let rec classify_not_term status no_dep_prods 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 _ -> - (classify_not_term status true context t : not_term :> [> not_term]) + (classify_not_term status context t : not_term :> [> not_term]) | ty -> let ty = fix_sorts ty in `Term - (match classify_not_term status true context ty with + (match classify_not_term status context ty with | `Proposition -> `Proof | `Type -> `Term | `KindOrType -> `TypeFormerOrTerm @@ -173,13 +262,12 @@ let rec kind_of status ~metasenv context k = | NCic.Sort NCic.Type _ -> Type | NCic.Sort _ -> assert false (* NOT A KIND *) | NCic.Prod (b,s,t) -> - (* CSC: non-invariant assumed here about "_" *) (match classify status ~metasenv context s with - | `Kind - | `KindOrType -> (* KindOrType OK?? *) + | `Kind -> KArrow (kind_of status ~metasenv context s, kind_of ~metasenv status ((b,NCic.Decl s)::context) t) | `Type + | `KindOrType | `Proposition | `PropKind -> KSkip (kind_of status ~metasenv ((b,NCic.Decl s)::context) t) @@ -212,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 @@ -243,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 ;; @@ -252,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 = @@ -273,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 = @@ -290,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 _)) @@ -312,37 +402,89 @@ 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 (* NOT A TYPE *) + | 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) @@ -369,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 @@ -400,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 = @@ -437,16 +620,50 @@ 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 *) ;; -let obj_of_constant status ~metasenv uri height bo ty = +type 'a result = + | Erased + | OutsideTheory + | Failure of string + | Success of 'a +;; + +let object_of_constant status ~metasenv ref bo ty = match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in @@ -464,185 +681,317 @@ let obj_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), - Some (uri,TypeDefinition((nicectx,res),bo)) - | `Kind -> status, None + (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, None - | `Term _ -> assert false (* IMPOSSIBLE *)) + | `Proposition -> status, Erased + | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.") | `PropKind - | `Proposition -> status, None + | `Proposition -> status, Erased | `KindOrType (* ??? *) | `Type -> (* CSC: TO BE FINISHED, REF NON REGISTERED *) let ty = typ_of status ~metasenv [] ty in status, - Some (uri, TermDefinition (split_typ_prods [] ty, - term_of status ~metasenv [] bo)) - | `Term _ -> assert false (* IMPOSSIBLE *) + 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 obj_of status (uri,height,metasenv,subst,obj_kind) = - let obj_kind = apply_subst subst obj_kind in - try - match obj_kind with - | NCic.Constant (_,_,None,ty,_) -> - (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), - Some (uri, TypeDeclaration res) - | `PropKind - | `Proposition -> status, None - | `Type - | `KindOrType (*???*) -> - let ty = typ_of status ~metasenv [] ty in - status, - Some (uri, TermDeclaration (split_typ_prods [] ty)) - | `Term _ -> assert false (* IMPOSSIBLE *)) - | NCic.Constant (_,_,Some bo,ty,_) -> - obj_of_constant status ~metasenv uri height bo ty - | NCic.Fixpoint (_fix_or_cofix,fs,_) -> - let status,objs = - List.fold_right - (fun (_,_name,_,ty,bo) (status,res) -> - let status,obj = obj_of_constant ~metasenv status uri height bo ty in - match obj with - None -> status,res (*CSC: PRETTY PRINT SOMETHING ERASED*) - | Some (_uri,obj) -> status,obj::res) - fs (status,[]) - in - status, Some (uri,LetRec objs) - | NCic.Inductive _ -> status,None (*CSC: TO BE IMPLEMENTED*) - with - NotInFOmega -> - prerr_endline "-- NOT IN F_omega"; - status, None +let object_of_inductive status ~metasenv uri ind leftno il = + let status,_,rev_tyl = + List.fold_left + (fun (status,i,res) (_,_,arity,cl) -> + match classify_not_term status [] arity with + | `Proposition + | `KindOrType + | `Type -> assert false (* IMPOSSIBLE *) + | `PropKind -> status,i+1,res + | `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 + (register_info status#extraction_db info) in + let cl = + 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 + NReference.mk_constructor (j+1) ref,ty + ) cl + in + status,i+1,([info],ref,left,right,cl)::res + ) (status,0,[]) il + in + match rev_tyl with + [] -> status,Erased + | _ -> 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 info = ref,(ctx,None) in + status#set_extraction_db + (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 ([],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 + object_of_constant status ~metasenv ref bo ty + | NCic.Fixpoint (fix_or_cofix,fs,_) -> + let _,status,objs = + List.fold_right + (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 (info,ref,obj) -> i+1,status, (info,ref,obj)::res + | _ -> i+1,status, res) fs (0,status,[]) + in + status, Success ([],dummyref,LetRec objs) + | NCic.Inductive (ind,leftno,il,_) -> + object_of_inductive status ~metasenv uri ind leftno il (************************ HASKELL *************************) +(* ----------------------------------------------------------------------------- + * Helper functions I can't seem to find anywhere in the OCaml stdlib? + * ----------------------------------------------------------------------------- + *) +let (|>) f g = + fun x -> g (f x) +;; + +let curry f x y = + f (x, y) +;; + +let uncurry f (x, y) = + f x y +;; + +let rec char_list_of_string s = + let l = String.length s in + let rec aux buffer s = + function + | 0 -> buffer + | m -> aux (s.[m - 1]::buffer) s (m - 1) + in + aux [] s l +;; + +let string_of_char_list s = + let rec aux buffer = + function + | [] -> buffer + | x::xs -> aux (String.make 1 x ^ buffer) xs + in + aux "" s +;; + +(* ---------------------------------------------------------------------------- + * Haskell name management: prettyfying valid and idiomatic Haskell identifiers + * and type variable names. + * ---------------------------------------------------------------------------- + *) + +let remove_underscores_and_mark = + let rec aux char_list_buffer positions_buffer position = + function + | [] -> (string_of_char_list char_list_buffer, positions_buffer) + | x::xs -> + if x == '_' then + aux char_list_buffer (position::positions_buffer) position xs + else + aux (x::char_list_buffer) positions_buffer (position + 1) xs + in + aux [] [] 0 +;; + +let rec capitalize_marked_positions s = + function + | [] -> s + | x::xs -> + if x < String.length s then + let c = Char.uppercase (String.get s x) in + let _ = String.set s x c in + capitalize_marked_positions s xs + else + capitalize_marked_positions s xs +;; + +let contract_underscores_and_capitalise = + char_list_of_string |> + remove_underscores_and_mark |> + uncurry capitalize_marked_positions +;; + +let idiomatic_haskell_type_name_of_string = + contract_underscores_and_capitalise |> + String.capitalize +;; + +let idiomatic_haskell_term_name_of_string = + contract_underscores_and_capitalise |> + 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 + 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 +;; let capitalize classification name = match classification with - `Constructor - | `TypeName -> String.capitalize name - | `FunctionName -> String.uncapitalize name + | `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 = +let rec (@:::) name l = if name <> "" (* propositional things *) && name.[0] = '_' then let name = String.sub name 1 (String.length name - 1) in let name = if name = "" then "a" else name in - name @:: l - else if List.mem name l then (name ^ "'") @:: l - else name::l + name @::: l + else if List.mem name l then (name ^ "'") @::: l + else name,l ;; -let rec pp_kind = - function - Type -> "*" - | KArrow (k1,k2) -> "(" ^ pp_kind k1 ^ ") -> " ^ pp_kind k2 - | KSkip k -> pp_kind k - -let rec pp_typ status ctx = - function - Var n -> List.nth ctx (n-1) - | Unit -> "()" - | Top -> assert false (* ??? *) - | TConst ref -> pp_ref status ref - | Arrow (t1,t2) -> "(" ^ pp_typ status ctx t1 ^ ") -> " ^ pp_typ status ("_"::ctx) t2 - | Skip t -> pp_typ status ("_"::ctx) t - | Forall (name,_,t) -> - (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) - let name = String.uncapitalize name in - "(forall " ^ name ^ ". " ^ pp_typ status (name@::ctx) t ^")" - | TAppl tl -> "(" ^ String.concat " " (List.map (pp_typ status ctx) tl) ^ ")" - -let rec pp_term status ctx = - function - Rel n -> List.nth ctx (n-1) - | UnitTerm -> "()" - | Const ref -> pp_ref status ref - | Lambda (name,t) -> "(\\" ^ name ^ " -> " ^ pp_term status (name@::ctx) t ^ ")" - | Appl tl -> "(" ^ String.concat " " (List.map (pp_term status ctx) tl) ^ ")" - | LetIn (name,s,t) -> - "(let " ^ name ^ " = " ^ pp_term status ctx s ^ " in " ^ pp_term status (name@::ctx) t ^ - ")" - | Match (r,matched,pl) -> - let constructors, leftno = - let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in - let _,_,_,cl = List.nth tys n in - cl,leftno - in - let rec eat_branch n ty pat = - match (ty, pat) with - | NCic.Prod (_, _, t), _ when n > 0 -> - eat_branch (pred n) t pat - | NCic.Prod (_, _, t), Lambda (name, t') -> - (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*) - let cv, rhs = eat_branch 0 t t' in - name :: cv, rhs - | _, _ -> [], pat - in - let j = ref 0 in - let patterns = - try - List.map2 - (fun (_, name, ty) pat -> - incr j; - name, eat_branch leftno ty pat - ) constructors pl - with Invalid_argument _ -> assert false - in - "case " ^ pp_term status ctx matched ^ " of\n" ^ - String.concat "\n" - (List.map - (fun (name,(bound_names,rhs)) -> - let pattern,body = - (*CSC: BUG avoid name clashes *) - String.concat " " (String.capitalize name::bound_names), - pp_term status ((List.rev bound_names)@ctx) rhs - in - " " ^ pattern ^ " -> " ^ body - ) patterns) - | TLambda t -> pp_term status ctx t - | Inst t -> pp_term status ctx t - -(* -type term_context = (string * [`OfKind of kind | `OfType of typ]) option list +let (@::) x l = let x,l = x @::: l in x::l;; -type term_former_def = term_context * term * typ -type term_former_decl = term_context * typ -*) +let rec pretty_print_type status ctxt = + function + | Var n -> List.nth ctxt (n-1) + | Unit -> "()" + | 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 + | TSkip t -> pretty_print_type status ("_"::ctxt) t + | Forall (name, kind, t) -> + (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) + 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 + else + "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) -> + 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 = 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 + "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 +;; -let rec pp_obj status (uri,obj_kind) = - let pp_ctx ctx = - String.concat " " (List.rev - (List.fold_right (fun (x,_) l -> x@::l) - (HExtlib.filter_map (fun x -> x) ctx) [])) in +let rec pp_obj status (_,ref,obj_kind) = + let pretty_print_context ctx = + String.concat " " (List.rev (snd + (List.fold_right + (fun (x,kind) (l,res) -> + let x,l = x @:::l in + if size_of_kind kind > 1 then + x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res + else + x::l,x::res) + (HExtlib.filter_map (fun x -> x) ctx) ([],[])))) + in let namectx_of_ctx ctx = List.fold_right (@::) (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in @@ -650,950 +999,80 @@ let rec pp_obj status (uri,obj_kind) = TypeDeclaration (ctx,_) -> (* data?? unsure semantics: inductive type without constructor, but not matchable apparently *) - "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx - | TypeDefinition ((ctx,_),ty) -> + if List.length ctx = 0 then + "data " ^ pp_ref status ref + else + "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx + | TypeDefinition ((ctx, _),ty) -> let namectx = namectx_of_ctx ctx in - "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^ - pp_typ status namectx ty + if List.length ctx = 0 then + "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty + else + "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty | TermDeclaration (ctx,ty) -> - (* Implemented with undefined, the best we can do *) - let name = name_of_uri `FunctionName uri in - name ^ " :: " ^ pp_typ status [] (glue_ctx_typ ctx ty) ^ "\n" ^ - name ^ " = undefined" + 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 - name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^ - name ^ " = " ^ pp_term status namectx bo + (*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 _,ref,left,right,cl -> + "data " ^ pp_ref status ref ^ " " ^ + pretty_print_context (right@left) ^ " where\n " ^ + String.concat "\n " (List.map + (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 haskell_of_obj status obj = - let status, obj = obj_of status obj in +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 - None -> "-- ERASED\n" - | Some obj -> pp_obj status obj ^ "\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 rec typ_of context = - function -(* - C.Rel n -> - begin - try - (match get_nth context n with - Some (C.Name s,_) -> ppid s - | Some (C.Anonymous,_) -> "__" ^ string_of_int n - | None -> "_hidden_" ^ string_of_int n - ) - with - NotEnoughElements -> string_of_int (List.length context - n) - end - | C.Meta (n,l1) -> - (match metasenv with - None -> - "?" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev_map - (function - None -> "_" - | Some t -> pp ~in_type:false t context) l1) ^ - "]" - | Some metasenv -> - try - let _,context,_ = CicUtil.lookup_meta n metasenv in - "?" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev - (List.map2 - (fun x y -> - match x,y with - _, None - | None, _ -> "_" - | Some _, Some t -> pp ~in_type:false t context - ) context l1)) ^ - "]" - with - CicUtil.Meta_not_found _ - | Invalid_argument _ -> - "???" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev_map (function None -> "_" | Some t -> - pp ~in_type:false t context) l1) ^ - "]" - ) - | C.Sort s -> - (match s with - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type _ -> "Type" - (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) - | C.CProp _ -> "CProp" - ) - | C.Implicit (Some `Hole) -> "%" - | C.Implicit _ -> "?" - | C.Prod (b,s,t) -> - (match b, is_term s with - _, true -> typ_of (None::context) t - | "_",_ -> Arrow (typ_of context s) (typ_of (Some b::context) t) - | _,_ -> Forall (b,typ_of (Some b::context) t) - | C.Lambda (b,s,t) -> - (match analyze_type context s with - `Sort _ - | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context) - | `Optimize -> prerr_endline "XXX lambda";assert false - | `Type -> - "(function " ^ ppname b ^ " -> " ^ - pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")") - | C.LetIn (b,s,ty,t) -> - (match analyze_term context s with - | `Type - | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) - | `Optimize - | `Term -> - "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*) - " = " ^ pp ~in_type:false s context ^ " in " ^ - pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")") - | C.Appl (he::tl) when in_type -> - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_ty context tl) in - (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes - | C.Appl (C.MutInd _ as he::tl) -> - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_ty context tl) in - (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes - | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) -> - let nparams = - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (_,_,nparams,_) -> nparams - | _ -> assert false in - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_constr nparams context tl) in - "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")" - | C.Appl li -> - "(" ^ String.concat " " (clean_args context li) ^ ")" - | C.Const (uri,exp_named_subst) -> - qualified_name_of_uri status current_module_uri uri ^ - pp_exp_named_subst exp_named_subst context - | C.MutInd (uri,n,exp_named_subst) -> - (try - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,_,_) -> - let (name,_,_,_) = get_nth dl (n+1) in - qualified_name_of_uri status current_module_uri - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^ - pp_exp_named_subst exp_named_subst context - | _ -> raise CicExportationInternalError - with - Sys.Break as exn -> raise exn - | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1) - ) - | C.MutConstruct (uri,n1,n2,exp_named_subst) -> - (try - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,_,_) -> - let _,_,_,cons = get_nth dl (n1+1) in - let id,_ = get_nth cons n2 in - qualified_name_of_uri status current_module_uri ~capitalize:true - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^ - pp_exp_named_subst exp_named_subst context - | _ -> raise CicExportationInternalError - with - Sys.Break as exn -> raise exn - | _ -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^ - string_of_int n2 - ) - | C.MutCase (uri,n1,ty,te,patterns) -> - if in_type then - "unit (* TOO POLYMORPHIC TYPE *)" - else ( - let rec needs_obj_magic ty = - match CicReduction.whd context ty with - | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t - | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t) - | _ -> false (* it can be a Rel, e.g. in *_rec *) - in - let needs_obj_magic = needs_obj_magic ty in - (match analyze_term context te with - `Type -> assert false - | `Proof -> - (match patterns with - [] -> "assert false" (* empty type elimination *) - | [he] -> - pp ~in_type:false he context (* singleton elimination *) - | _ -> assert false) - | `Optimize - | `Term -> - if patterns = [] then "assert false" - else - (let connames_and_argsno, go_up, go_pu, go_down, go_nwod = - (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,paramsno,_) -> - let (_,_,_,cons) = get_nth dl (n1+1) in - let rc = - List.map - (fun (id,ty) -> - (* this is just an approximation since we do not have - reduction yet! *) - let rec count_prods toskip = - function - C.Prod (_,_,bo) when toskip > 0 -> - count_prods (toskip - 1) bo - | C.Prod (_,_,bo) -> 1 + count_prods 0 bo - | _ -> 0 - in - qualified_name_of_uri status current_module_uri - ~capitalize:true - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), - count_prods paramsno ty - ) cons - in - if not (is_mcu_type uri) then rc, "","","","" - else rc, !current_go_up, "))", "( .< (", " ) >.)" - | _ -> raise CicExportationInternalError - ) - in - let connames_and_argsno_and_patterns = - let rec combine = - function - [],[] -> [] - | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly)) - | _,_ -> assert false - in - combine (connames_and_argsno,patterns) - in - go_up ^ - "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^ - (String.concat "\n | " - (List.map - (fun (x,argsno,y) -> - let rec aux argsno context = - function - Cic.Lambda (name,ty,bo) when argsno > 0 -> - let name = - match name with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name n -> Cic.Name (ppid n) in - let args,res = - aux (argsno - 1) (Some (name,Cic.Decl ty)::context) - bo - in - (match analyze_type context ty with - | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false - | `Statement - | `Sort _ -> args,res - | `Type -> - (match name with - C.Anonymous -> "_" - | C.Name s -> s)::args,res) - | t when argsno = 0 -> [],pp ~in_type:false t context - | t -> - ["{" ^ string_of_int argsno ^ " args missing}"], - pp ~in_type:false t context - in - let pattern,body = - if argsno = 0 then x,pp ~in_type:false y context - else - let args,body = aux argsno context y in - let sargs = String.concat "," args in - x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), - body - in - pattern ^ " -> " ^ go_down ^ - (if needs_obj_magic then - "Obj.magic (" ^ body ^ ")" - else - body) ^ go_nwod - ) connames_and_argsno_and_patterns)) ^ - ")\n"^go_pu))) - | C.Fix (no, funs) -> - let names,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) funs - in - "let rec " ^ - List.fold_right - (fun (name,ind,ty,bo) i -> name ^ " = \n" ^ - pp ~in_type:false bo (names@context) ^ i) - funs "" ^ - " in " ^ - (match get_nth names (no + 1) with - Some (Cic.Name n,_) -> n - | _ -> assert false) - | C.CoFix (no,funs) -> - let names,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) funs - in - "\nCoFix " ^ " {" ^ - List.fold_right - (fun (name,ty,bo) i -> "\n" ^ name ^ - " : " ^ pp ~in_type:true ty context ^ " := \n" ^ - pp ~in_type:false bo (names@context) ^ i) - funs "" ^ - "}\n" -*) - -(* -exception CicExportationInternalError;; -exception NotEnoughElements;; - -(* *) - -let is_mcu_type u = - UriManager.eq (UriManager.uri_of_string - "cic:/matita/freescale/opcode/mcu_type.ind") u -;; - -(* Utility functions *) - -let analyze_term context t = - match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with - | Cic.Sort _ -> `Type - | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize - | ty -> - match - fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph) - with - | Cic.Sort Cic.Prop -> `Proof - | _ -> `Term -;; - -let analyze_type context t = - let rec aux = +let refresh_uri_in_typ ~refresh_uri_in_reference = + let rec refresh_uri_in_typ = function - Cic.Sort s -> `Sort s - | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize - | Cic.Prod (_,_,t) -> aux t - | _ -> `SomethingElse + | 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 - match aux t with - `Sort _ | `Optimize as res -> res - | `SomethingElse -> - match - fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph) - with - Cic.Sort Cic.Prop -> `Statement - | _ -> `Type -;; - -let ppid = - let reserved = - [ "to"; - "mod"; - "val"; - "in"; - "function" - ] - in - function n -> - let n = String.uncapitalize n in - if List.mem n reserved then n ^ "_" else n -;; - -let ppname = - function - Cic.Name s -> ppid s - | Cic.Anonymous -> "_" -;; - -(* get_nth l n returns the nth element of the list l if it exists or *) -(* raises NotEnoughElements if l has less than n elements *) -let rec get_nth l n = - match (n,l) with - (1, he::_) -> he - | (n, he::tail) when n > 1 -> get_nth tail (n-1) - | (_,_) -> raise NotEnoughElements -;; - -let qualified_name_of_uri status current_module_uri ?(capitalize=false) uri = - let name = - if capitalize then - String.capitalize (UriManager.name_of_uri status uri) - else - ppid (UriManager.name_of_uri status uri) in - let filename = - let suri = UriManager.buri_of_uri uri in - let s = String.sub suri 5 (String.length suri - 5) in - let s = Pcre.replace ~pat:"/" ~templ:"_" s in - String.uncapitalize s in - if current_module_uri = UriManager.buri_of_uri uri then - name - else - String.capitalize filename ^ "." ^ name -;; - -let current_go_up = ref "(.!(";; -let at_level2 f x = - try - current_go_up := "(.~("; - let rc = f x in - current_go_up := "(.!("; - rc - with exn -> - current_go_up := "(.!("; - raise exn -;; - -let pp current_module_uri ?metasenv ~in_type = -let rec pp ~in_type t context = - let module C = Cic in - match t with - C.Rel n -> - begin - try - (match get_nth context n with - Some (C.Name s,_) -> ppid s - | Some (C.Anonymous,_) -> "__" ^ string_of_int n - | None -> "_hidden_" ^ string_of_int n - ) - with - NotEnoughElements -> string_of_int (List.length context - n) - end - | C.Var (uri,exp_named_subst) -> - qualified_name_of_uri status current_module_uri uri ^ - pp_exp_named_subst exp_named_subst context - | C.Meta (n,l1) -> - (match metasenv with - None -> - "?" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev_map - (function - None -> "_" - | Some t -> pp ~in_type:false t context) l1) ^ - "]" - | Some metasenv -> - try - let _,context,_ = CicUtil.lookup_meta n metasenv in - "?" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev - (List.map2 - (fun x y -> - match x,y with - _, None - | None, _ -> "_" - | Some _, Some t -> pp ~in_type:false t context - ) context l1)) ^ - "]" - with - CicUtil.Meta_not_found _ - | Invalid_argument _ -> - "???" ^ (string_of_int n) ^ "[" ^ - String.concat " ; " - (List.rev_map (function None -> "_" | Some t -> - pp ~in_type:false t context) l1) ^ - "]" - ) - | C.Sort s -> - (match s with - C.Prop -> "Prop" - | C.Set -> "Set" - | C.Type _ -> "Type" - (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) - | C.CProp _ -> "CProp" - ) - | C.Implicit (Some `Hole) -> "%" - | C.Implicit _ -> "?" - | C.Prod (b,s,t) -> - (match b with - C.Name n -> - let n = "'" ^ String.uncapitalize n in - "(" ^ pp ~in_type:true s context ^ " -> " ^ - pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")" - | C.Anonymous -> - "(" ^ pp ~in_type:true s context ^ " -> " ^ - pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")") - | C.Cast (v,t) -> pp ~in_type v context - | C.Lambda (b,s,t) -> - (match analyze_type context s with - `Sort _ - | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context) - | `Optimize -> prerr_endline "XXX lambda";assert false - | `Type -> - "(function " ^ ppname b ^ " -> " ^ - pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")") - | C.LetIn (b,s,ty,t) -> - (match analyze_term context s with - | `Type - | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) - | `Optimize - | `Term -> - "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*) - " = " ^ pp ~in_type:false s context ^ " in " ^ - pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) ^ ")") - | C.Appl (he::tl) when in_type -> - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_ty context tl) in - (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes - | C.Appl (C.MutInd _ as he::tl) -> - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_ty context tl) in - (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes - | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) -> - let nparams = - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (_,_,nparams,_) -> nparams - | _ -> assert false in - let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args_for_constr nparams context tl) in - "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")" - | C.Appl li -> - "(" ^ String.concat " " (clean_args context li) ^ ")" - | C.Const (uri,exp_named_subst) -> - qualified_name_of_uri status current_module_uri uri ^ - pp_exp_named_subst exp_named_subst context - | C.MutInd (uri,n,exp_named_subst) -> - (try - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,_,_) -> - let (name,_,_,_) = get_nth dl (n+1) in - qualified_name_of_uri status current_module_uri - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con")) ^ - pp_exp_named_subst exp_named_subst context - | _ -> raise CicExportationInternalError - with - Sys.Break as exn -> raise exn - | _ -> UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n + 1) - ) - | C.MutConstruct (uri,n1,n2,exp_named_subst) -> - (try - match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,_,_) -> - let _,_,_,cons = get_nth dl (n1+1) in - let id,_ = get_nth cons n2 in - qualified_name_of_uri status current_module_uri ~capitalize:true - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")) ^ - pp_exp_named_subst exp_named_subst context - | _ -> raise CicExportationInternalError - with - Sys.Break as exn -> raise exn - | _ -> - UriManager.string_of_uri uri ^ "#1/" ^ string_of_int (n1 + 1) ^ "/" ^ - string_of_int n2 - ) - | C.MutCase (uri,n1,ty,te,patterns) -> - if in_type then - "unit (* TOO POLYMORPHIC TYPE *)" - else ( - let rec needs_obj_magic ty = - match CicReduction.whd context ty with - | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t - | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t) - | _ -> false (* it can be a Rel, e.g. in *_rec *) - in - let needs_obj_magic = needs_obj_magic ty in - (match analyze_term context te with - `Type -> assert false - | `Proof -> - (match patterns with - [] -> "assert false" (* empty type elimination *) - | [he] -> - pp ~in_type:false he context (* singleton elimination *) - | _ -> assert false) - | `Optimize - | `Term -> - if patterns = [] then "assert false" - else - (let connames_and_argsno, go_up, go_pu, go_down, go_nwod = - (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with - C.InductiveDefinition (dl,_,paramsno,_) -> - let (_,_,_,cons) = get_nth dl (n1+1) in - let rc = - List.map - (fun (id,ty) -> - (* this is just an approximation since we do not have - reduction yet! *) - let rec count_prods toskip = - function - C.Prod (_,_,bo) when toskip > 0 -> - count_prods (toskip - 1) bo - | C.Prod (_,_,bo) -> 1 + count_prods 0 bo - | _ -> 0 - in - qualified_name_of_uri status current_module_uri - ~capitalize:true - (UriManager.uri_of_string - (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), - count_prods paramsno ty - ) cons - in - if not (is_mcu_type uri) then rc, "","","","" - else rc, !current_go_up, "))", "( .< (", " ) >.)" - | _ -> raise CicExportationInternalError - ) - in - let connames_and_argsno_and_patterns = - let rec combine = - function - [],[] -> [] - | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly)) - | _,_ -> assert false - in - combine (connames_and_argsno,patterns) - in - go_up ^ - "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^ - (String.concat "\n | " - (List.map - (fun (x,argsno,y) -> - let rec aux argsno context = - function - Cic.Lambda (name,ty,bo) when argsno > 0 -> - let name = - match name with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name n -> Cic.Name (ppid n) in - let args,res = - aux (argsno - 1) (Some (name,Cic.Decl ty)::context) - bo - in - (match analyze_type context ty with - | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false - | `Statement - | `Sort _ -> args,res - | `Type -> - (match name with - C.Anonymous -> "_" - | C.Name s -> s)::args,res) - | t when argsno = 0 -> [],pp ~in_type:false t context - | t -> - ["{" ^ string_of_int argsno ^ " args missing}"], - pp ~in_type:false t context - in - let pattern,body = - if argsno = 0 then x,pp ~in_type:false y context - else - let args,body = aux argsno context y in - let sargs = String.concat "," args in - x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), - body - in - pattern ^ " -> " ^ go_down ^ - (if needs_obj_magic then - "Obj.magic (" ^ body ^ ")" - else - body) ^ go_nwod - ) connames_and_argsno_and_patterns)) ^ - ")\n"^go_pu))) - | C.Fix (no, funs) -> - let names,_ = - List.fold_left - (fun (types,len) (n,_,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) funs - in - "let rec " ^ - List.fold_right - (fun (name,ind,ty,bo) i -> name ^ " = \n" ^ - pp ~in_type:false bo (names@context) ^ i) - funs "" ^ - " in " ^ - (match get_nth names (no + 1) with - Some (Cic.Name n,_) -> n - | _ -> assert false) - | C.CoFix (no,funs) -> - let names,_ = - List.fold_left - (fun (types,len) (n,ty,_) -> - (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, - len+1) - ) ([],0) funs - in - "\nCoFix " ^ " {" ^ - List.fold_right - (fun (name,ty,bo) i -> "\n" ^ name ^ - " : " ^ pp ~in_type:true ty context ^ " := \n" ^ - pp ~in_type:false bo (names@context) ^ i) - funs "" ^ - "}\n" -and pp_exp_named_subst exp_named_subst context = - if exp_named_subst = [] then "" else - "\\subst[" ^ - String.concat " ; " ( - List.map - (function (uri,t) -> UriManager.name_of_uri status uri ^ " \\Assign " ^ pp ~in_type:false t context) - exp_named_subst - ) ^ "]" -and clean_args_for_constr nparams context = - let nparams = ref nparams in - HExtlib.filter_map - (function t -> - decr nparams; - match analyze_term context t with - `Term when !nparams < 0 -> Some (pp ~in_type:false t context) - | `Optimize - | `Term - | `Type - | `Proof -> None) -and clean_args context = - function - | [] | [_] -> assert false - | he::arg1::tl as l -> - let head_arg1, rest = - match analyze_term context arg1 with - | `Optimize -> - !current_go_up :: pp ~in_type:false he context :: - pp ~in_type:false arg1 context :: ["))"], tl - | _ -> [], l + 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 - head_arg1 @ - HExtlib.filter_map - (function t -> - match analyze_term context t with - | `Term -> Some (pp ~in_type:false t context) - | `Optimize -> - prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false - | `Type - | `Proof -> None) rest -and clean_args_for_ty context = - HExtlib.filter_map - (function t -> - match analyze_term context t with - `Type -> Some (pp ~in_type:true t context) - | `Optimize -> None - | `Proof -> None - | `Term -> None) -in - pp ~in_type -;; - -let ppty current_module_uri = - (* nparams is the number of left arguments - left arguments should either become parameters or be skipped altogether *) - let rec args nparams context = - function - Cic.Prod (n,s,t) -> - let n = - match n with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name n -> Cic.Name (String.uncapitalize n) - in - (match analyze_type context s with - | `Optimize - | `Statement - | `Sort Cic.Prop -> - args (nparams - 1) ((Some (n,Cic.Decl s))::context) t - | `Type when nparams > 0 -> - args (nparams - 1) ((Some (n,Cic.Decl s))::context) t - | `Type -> - let abstr,args = - args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in - abstr,pp ~in_type:true current_module_uri s context::args - | `Sort _ when nparams <= 0 -> - let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in - args (nparams - 1) ((Some (n,Cic.Decl s))::context) t - | `Sort _ -> - let n = - match n with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name name -> Cic.Name ("'" ^ name) in - let abstr,args = - args (nparams - 1) ((Some (n,Cic.Decl s))::context) t - in - (match n with - Cic.Anonymous -> abstr - | Cic.Name name -> name::abstr), - args) - | _ -> [],[] - in - args -;; - -exception DoNotExtract;; - -let pp_abstracted_ty current_module_uri = - let rec args context = - function - Cic.Lambda (n,s,t) -> - let n = - match n with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name n -> Cic.Name (String.uncapitalize n) - in - (match analyze_type context s with - | `Optimize - | `Statement - | `Type - | `Sort Cic.Prop -> - args ((Some (n,Cic.Decl s))::context) t - | `Sort _ -> - let n = - match n with - Cic.Anonymous -> Cic.Anonymous - | Cic.Name name -> Cic.Name ("'" ^ name) in - let abstr,res = - args ((Some (n,Cic.Decl s))::context) t - in - (match n with - Cic.Anonymous -> abstr - | Cic.Name name -> name::abstr), - res) - | ty -> - match analyze_type context ty with - | `Optimize -> - prerr_endline "XXX abstracted l2 ty"; assert false - | `Sort _ - | `Statement -> raise DoNotExtract - | `Type -> - (* BUG HERE: this can be a real System F type *) - let head = pp ~in_type:true current_module_uri ty context in - [],head - in - args -;; - - -(* ppinductiveType (typename, inductive, arity, cons) *) -(* pretty-prints a single inductive definition *) -(* (typename, inductive, arity, cons) *) -let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons) -= - match analyze_type [] arity with - `Sort Cic.Prop -> "" - | `Optimize - | `Statement - | `Type -> assert false - | `Sort _ -> - if cons = [] then - "type " ^ String.uncapitalize typename ^ " = unit (* empty type *)\n" - else ( - let abstr,scons = - List.fold_right - (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *) - let abstr',sargs = ppty current_module_uri nparams [] ty in - let sargs = String.concat " * " sargs in - abstr', - String.capitalize id ^ - (if sargs = "" then "" else " of " ^ sargs) ^ - (if i = "" then "" else "\n | ") ^ i) - cons ([],"") - in - let abstr = - let s = String.concat "," abstr in - if s = "" then "" else "(" ^ s ^ ") " - in - "type " ^ abstr ^ String.uncapitalize typename ^ " =\n" ^ scons ^ "\n") -;; - -let ppobj current_module_uri obj = - let module C = Cic in - let module U = UriManager in - let pp ~in_type = pp ~in_type current_module_uri in - match obj with - C.Constant (name, Some t1, t2, params, _) -> - (match analyze_type [] t2 with - | `Sort Cic.Prop - | `Statement -> "" - | `Optimize - | `Type -> - (match t1 with - | Cic.Lambda (Cic.Name arg, s, t) -> - (match analyze_type [] s with - | `Optimize -> - - "let " ^ ppid name ^ "__1 = function " ^ ppid arg - ^ " -> .< " ^ - at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)] - ^ " >. ;;\n" - ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n" - ^ "let " ^ ppid name ^ " = function " ^ ppid arg - ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic !"^ppid name - ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic (" - ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!" - ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!" - ^ppid name^"__2)) >.\n;;\n" - ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid - name^" Matita_freescale_opcode.HCS08)" - | _ -> - "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n") - | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n") - | `Sort _ -> - match analyze_type [] t1 with - `Sort Cic.Prop -> "" - | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false - | _ -> - (try - let abstr,res = pp_abstracted_ty current_module_uri [] t1 in - let abstr = - let s = String.concat "," abstr in - if s = "" then "" else "(" ^ s ^ ") " - in - "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n" - with - DoNotExtract -> "")) - | C.Constant (name, None, ty, params, _) -> - (match analyze_type [] ty with - `Sort Cic.Prop - | `Optimize -> prerr_endline "XXX axiom l2"; assert false - | `Statement -> "" - | `Sort _ -> "type " ^ ppid name ^ "\n" - | `Type -> "let " ^ ppid name ^ " = assert false\n") - | C.Variable (name, bo, ty, params, _) -> - "Variable " ^ name ^ - "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ - ")" ^ ":\n" ^ - pp ~in_type:true ty [] ^ "\n" ^ - (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo []) - | C.CurrentProof (name, conjectures, value, ty, params, _) -> - "Current Proof of " ^ name ^ - "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^ - ")" ^ ":\n" ^ - let separate s = if s = "" then "" else s ^ " ; " in - List.fold_right - (fun (n, context, t) i -> - let conjectures',name_context = - List.fold_right - (fun context_entry (i,name_context) -> - (match context_entry with - Some (n,C.Decl at) -> - (separate i) ^ - ppname n ^ ":" ^ - pp ~in_type:true ~metasenv:conjectures - at name_context ^ " ", - context_entry::name_context - | Some (n,C.Def (at,aty)) -> - (separate i) ^ - ppname n ^ ":" ^ - pp ~in_type:true ~metasenv:conjectures - aty name_context ^ - ":= " ^ pp ~in_type:false - ~metasenv:conjectures at name_context ^ " ", - context_entry::name_context - | None -> - (separate i) ^ "_ :? _ ", context_entry::name_context) - ) context ("",[]) - in - conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^ - pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i - ) conjectures "" ^ - "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^ - pp ~in_type:true ~metasenv:conjectures ty [] - | C.InductiveDefinition (l, params, nparams, _) -> - List.fold_right - (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l "" -;; - -let ppobj current_module_uri obj = - let res = ppobj current_module_uri obj in - if res = "" then "" else res ^ ";;\n\n" -;; -*) -*) + refresh_uri_in_reference ref,(ctx,typ)) + infos