X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=7b24f74c0c741b799f29dd6d95f7318bd1eac82f;hb=87e64004d2fb44077b68c4f9c009223b81ad2b6d;hp=ec2d1c1c3ec271148a985c22adb5a1980779793f;hpb=de80dc03fc495c4dbdb54a970645dae34cbed1e7;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index ec2d1c1c3..7b24f74c0 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -32,31 +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 - | 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 - | 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 bracket size_of pp o = + if size_of o > 1 then + "(" ^ pp o ^ ")" + else + pp o +;; -let unitty = - NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));; +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 v -> 1 + | Unit -> 1 + | Top -> 1 + | TConst c -> 1 + | Arrow _ -> 2 + | TSkip t -> size_of_type t + | Forall _ -> 2 + | TAppl l -> 1 +;; (* None = dropped abstraction *) type typ_context = (string * kind) option list @@ -65,36 +86,73 @@ 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 r -> 1 + | UnitTerm -> 1 + | Const c -> 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 +;; +let unitty = + NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));; + 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 (string * typ * term) list - (* inductive and records missing *) + | LetRec of (NReference.reference * obj_kind) list + (* reference, left, right, constructors *) + | Algebraic of (NReference.reference * typ_context * typ_context * (NReference.reference * typ) list) list -type obj = NUri.uri * obj_kind +type obj = NReference.reference * obj_kind -exception NotInFOmega +(* For LetRec and Algebraic blocks *) +let dummyref = + NReference.reference_of_string "cic:/matita/dummy/dummy.ind(1,1,1)" -let rec classify_not_term status no_dep_prods context t = +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 _ @@ -105,7 +163,7 @@ let rec classify_not_term status no_dep_prods context t = (* be aware: we can be the head of an application *) assert false (* TODO *) | NCic.Meta _ -> assert false (* TODO *) - | NCic.Appl (he::_) -> classify_not_term status no_dep_prods context he + | 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 @@ -128,16 +186,16 @@ 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 - | `KindOrType -> `KindOrType + | `KindOrType -> `Type | `PropKind -> `Proposition) | 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 *) @@ -153,11 +211,11 @@ 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 @@ -171,13 +229,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) @@ -202,16 +259,17 @@ let rec skip_args status ~metasenv context = match classify status ~metasenv context arg with | `KindOrType | `Type - | `Term `TypeFormer -> arg::skip_args status ~metasenv context (tl1,tl2) + | `Term `TypeFormer -> + Some arg::skip_args status ~metasenv context (tl1,tl2) | `Kind | `Proposition - | `PropKind -> unitty::skip_args status ~metasenv context (tl1,tl2) + | `PropKind -> None::skip_args status ~metasenv context (tl1,tl2) | `Term _ -> assert false (* IMPOSSIBLE *) ;; module ReferenceMap = Map.Make(struct type t = NReference.reference let compare = NReference.compare end) -type db = typ_context ReferenceMap.t +type db = (typ_context * typ option) ReferenceMap.t class type g_status = object @@ -240,7 +298,7 @@ let rec split_typ_prods context = function | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta - | Skip ta -> split_typ_prods (None::context) ta + | TSkip ta -> split_typ_prods (None::context) ta | _ as t -> context,t ;; @@ -249,7 +307,7 @@ let rec glue_ctx_typ ctx typ = | [] -> typ | Some (_,`OfType so)::ctx -> glue_ctx_typ ctx (Arrow (so,typ)) | Some (name,`OfKind so)::ctx -> glue_ctx_typ ctx (Forall (name,so,typ)) - | None::ctx -> glue_ctx_typ ctx (Skip typ) + | None::ctx -> glue_ctx_typ ctx (TSkip typ) ;; let rec split_typ_lambdas status n ~metasenv context typ = @@ -276,9 +334,11 @@ let context_of_typformer status ~metasenv context = | NCic.Const (NReference.Ref (_,NReference.Def _) as ref) | NCic.Const (NReference.Ref (_,NReference.Decl) as ref) | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) -> - (try ReferenceMap.find ref status#extraction_db + (try fst (ReferenceMap.find ref status#extraction_db) with - Not_found -> assert false (* IMPOSSIBLE *)) + Not_found -> + prerr_endline ("REF NOT FOUND: " ^ NReference.string_of_reference ref); + assert false (* IMPOSSIBLE *)) | NCic.Match _ -> assert false (* TODO ???? *) | NCic.Rel n -> let typ = @@ -309,18 +369,19 @@ 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.Appl (he::args) -> let he_context = context_of_typformer status ~metasenv context he in TAppl (typ_of status ~metasenv context he :: - List.map (typ_of status ~metasenv context) + List.map + (function None -> Unit | Some ty -> typ_of status ~metasenv context ty) (skip_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 *) @@ -328,6 +389,34 @@ let rec typ_of status ~metasenv context k = | NCic.Match (_,_,_,_) -> assert false (* TODO *) ;; +let rec fomega_subst k t1 = + function + | Var n -> + if k=n then 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) + | TSkip t -> TSkip (fomega_subst (k+1) t1 t) + | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t) + | TAppl args -> TAppl (List.map (fomega_subst k t1) args) + +let fomega_lookup status ref = snd (ReferenceMap.find ref status#extraction_db) + +let rec fomega_whd status ty = + match ty with + | TConst r -> + (match fomega_lookup status r with + None -> ty + | Some ty -> fomega_whd status ty) + | TAppl (TConst r::args) -> + (match fomega_lookup status r with + None -> ty + | Some ty -> fomega_whd status (List.fold_right (fomega_subst 1) args ty)) + | _ -> ty + let rec term_of status ~metasenv context = function | NCic.Implicit _ @@ -337,17 +426,18 @@ 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 + | `Term `TypeFormerOrTerm (* ???? *) | `Term `Term -> LetIn (b,term_of status ~metasenv context t, term_of status ~metasenv ((b,NCic.Def (t,ty))::context) bo) @@ -358,1110 +448,482 @@ let rec term_of status ~metasenv context = | `Proposition | `Term `PropFormer | `Term `TypeFormer - | `Term `TypeFormerOrTerm - | `Term `Proof -> assert false (* NOT IN PROGRAMMING LANGUAGES? EXPAND IT ??? *)) + | `Term `Proof -> + (* not in programming languages, we expand it *) + term_of status ~metasenv context + (NCicSubstitution.subst status ~avoid_beta_redexes:true t bo)) | NCic.Rel n -> Rel n | NCic.Const ref -> Const ref | NCic.Appl (he::args) -> - assert false (* TODO - let he_context = context_of_typformer status ~metasenv context he in - TAppl (typ_of status ~metasenv context he :: - List.map (typ_of status ~metasenv context) - (skip_args status ~metasenv context (List.rev he_context,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 | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; otherwise NOT A TYPE *) | NCic.Meta _ -> assert false (* TODO *) | NCic.Match (ref,_,t,pl) -> - Match (ref,term_of status ~metasenv context t, - List.map (term_of status ~metasenv context) pl) + let patterns_of pl = + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status ref in + let _,_,_,cl = List.nth tys n in + cl,leftno + in + let rec eat_branch n ty context ctx pat = + match (ty, pat) with + | TSkip t,_ + | Forall (_,_,t),_ + | Arrow (_, t), _ when n > 0 -> + eat_branch (pred n) t context ctx pat + | _, _ when n > 0 -> assert false (*BUG: is Top possible here?*) + (*CSC: unify the three cases below? *) + | Arrow (_, t), NCic.Lambda (name, ty, t') -> + let ctx = + (Some (name,`OfType (typ_of status ~metasenv context ty)))::ctx in + let context = (name,NCic.Decl ty)::context in + eat_branch 0 t context ctx t' + | Forall (_,_,t),NCic.Lambda (name, ty, t') -> + let ctx = + (Some (name,`OfKind (kind_of status ~metasenv context ty)))::ctx in + let context = (name,NCic.Decl ty)::context in + eat_branch 0 t context ctx t' + | TSkip t,NCic.Lambda (name, ty, t') -> + let ctx = None::ctx in + let context = (name,NCic.Decl ty)::context in + eat_branch 0 t context ctx t' + | Top,_ -> assert false (*TODO: HOW??*) + (*BUG here, eta-expand!*) + | _, _ -> context,ctx, pat + in + try + List.map2 + (fun (_, name, ty) pat -> + (*BUG: recomputing every time the type of the constructor*) + let ty = typ_of status ~metasenv context ty in + let context,lhs,rhs = eat_branch leftno ty context [] pat in + let rhs = + (* UnsafeCoerce not always required *) + UnsafeCoerce (term_of status ~metasenv context rhs) + in + lhs,rhs + ) constructors pl + with Invalid_argument _ -> assert false + in + (match classify_not_term status [] (NCic.Const ref) with + | `PropKind + | `KindOrType + | `Kind -> assert false (* IMPOSSIBLE *) + | `Proposition -> + (match patterns_of pl with + [] -> BottomElim + | [_lhs,rhs] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*) + | _ -> assert false) + | `Type -> + Match (ref,term_of status ~metasenv context t, patterns_of pl)) +and eat_args status metasenv acc context tyhe = + function + [] -> acc + | arg::tl -> + match fomega_whd status tyhe with + Arrow (s,t) -> + let arg = + match s with + Unit -> UnitTerm + | _ -> term_of status ~metasenv context arg in + eat_args status metasenv (mk_appl acc arg) context t tl + | Forall (_,_,t) -> + 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 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 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,_) -> - (match classify status ~metasenv [] ty with - | `Kind -> - let ty = kind_of status ~metasenv [] ty in - let ctx0,res = split_kind_prods [] ty in - let ctx,bo = - split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in - (match classify status ~metasenv ctx bo with - | `Type - | `KindOrType -> (* ?? no kind formers in System F_omega *) - let nicectx = - List.map2 - (fun p1 n -> - HExtlib.map_option (fun (_,k) -> - (*CSC: BUG here, clashes*) - String.uncapitalize (fst n),k) p1) - ctx0 ctx - in - let ref = - NReference.reference_of_spec uri (NReference.Def height) in - status#set_extraction_db - (ReferenceMap.add ref ctx0 status#extraction_db), - Some (uri,TypeDefinition((nicectx,res),typ_of status ~metasenv ctx bo)) - | `Kind -> status, None - | `PropKind - | `Proposition -> status, None - | `Term _ -> assert false (* IMPOSSIBLE *)) - | `PropKind - | `Proposition -> status, None - | `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 *)) - with - NotInFOmega -> - prerr_endline "NOT IN F_omega"; - status, None - -(************************ HASKELL *************************) +type 'a result = + | Erased + | OutsideTheory + | Failure of string + | Success of 'a +;; -(*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 +let object_of_constant status ~metasenv ref bo ty = + match classify status ~metasenv [] ty with + | `Kind -> + let ty = kind_of status ~metasenv [] ty in + let ctx0,res = split_kind_prods [] ty in + let ctx,bo = + split_typ_lambdas status ~metasenv (List.length ctx0) [] bo in + (match classify status ~metasenv ctx bo with + | `Type + | `KindOrType -> (* ?? no kind formers in System F_omega *) + let nicectx = + List.map2 + (fun p1 n -> + HExtlib.map_option (fun (_,k) -> + (*CSC: BUG here, clashes*) + String.uncapitalize (fst n),k) p1) + ctx0 ctx + in + let bo = typ_of status ~metasenv ctx bo in + status#set_extraction_db + (ReferenceMap.add ref (nicectx,Some bo) + status#extraction_db), + Success (ref,TypeDefinition((nicectx,res),bo)) + | `Kind -> status, Erased (* DPM: but not really, more a failure! *) + | `PropKind + | `Proposition -> status, Erased + | `Term _ -> status, Failure "Body of type lambda classified as a term. This is a bug.") + | `PropKind + | `Proposition -> status, Erased + | `KindOrType (* ??? *) + | `Type -> + (* CSC: TO BE FINISHED, REF NON REGISTERED *) + let ty = typ_of status ~metasenv [] ty in + status, + 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 capitalize classification name = - match classification with - `Constructor - | `TypeName -> String.capitalize name - | `FunctionName -> String.uncapitalize name +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 + let status = + status#set_extraction_db + (ReferenceMap.add ref (ctx,None) status#extraction_db) 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,(ref,left,right,cl)::res + ) (status,0,[]) il + in + match rev_tyl with + [] -> status,Erased + | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl)) +;; -let pp_ref status ref = - capitalize (classify_reference status ref) - (NCicPp.r2s status false ref) +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 + status#set_extraction_db + (ReferenceMap.add ref (ctx,None) status#extraction_db), + Success (ref, TypeDeclaration res) + | `PropKind + | `Proposition -> status, Erased + | `Type + | `KindOrType (*???*) -> + let ty = typ_of status ~metasenv [] ty in + status, Success (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 (ref,obj) -> i+1,status, (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 -let name_of_uri classification uri = - capitalize classification (NUri.name_of_uri uri) +(************************ HASKELL *************************) -(* cons avoid duplicates *) -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 +(* ----------------------------------------------------------------------------- + * Helper functions I can't seem to find anywhere in the OCaml stdlib? + * ----------------------------------------------------------------------------- + *) +let (|>) f g = + fun x -> g (f x) ;; -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) - | 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) - | 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 _ -> assert false (* TODO of reference * term * term list *) - | 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 - -type term_former_def = term_context * term * typ -type term_former_decl = term_context * typ -*) +let curry f x y = + f (x, y) +;; -let 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 namectx_of_ctx ctx = - List.fold_right (@::) - (List.map (function None -> "" | Some (x,_) -> x) ctx) [] in - match obj_kind with - 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) -> - let namectx = namectx_of_ctx ctx in - "type " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^ - pp_typ 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" - | TermDefinition ((ctx,ty),bo) -> - let name = name_of_uri `FunctionName uri 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 - | LetRec _ -> assert false (* TODO - (* inductive and records missing *)*) +let uncurry f (x, y) = + f x y +;; -let haskell_of_obj status obj = - let status, obj = obj_of status obj in - status,HExtlib.map_option (pp_obj status) obj +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 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 +let string_of_char_list s = + let rec aux buffer = + function + | [] -> buffer + | x::xs -> aux (String.make 1 x ^ buffer) xs + in + aux "" s ;; -(* 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 +(* ---------------------------------------------------------------------------- + * 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 analyze_type context t = - let rec aux = +let rec capitalize_marked_positions s = function - Cic.Sort s -> `Sort s - | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize - | Cic.Prod (_,_,t) -> aux t - | _ -> `SomethingElse - 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 + | [] -> 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 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 contract_underscores_and_capitalise = + char_list_of_string |> + remove_underscores_and_mark |> + uncurry capitalize_marked_positions ;; -let ppname = - function - Cic.Name s -> ppid s - | Cic.Anonymous -> "_" +let idiomatic_haskell_type_name_of_string = + contract_underscores_and_capitalise |> + String.capitalize ;; -(* 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 idiomatic_haskell_term_name_of_string = + contract_underscores_and_capitalise |> + String.uncapitalize ;; -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 +(*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 - String.capitalize filename ^ "." ^ name + let NReference.Ref (_,ref) = ref in + match ref with + NReference.Con _ -> `Constructor + | NReference.Ind _ -> assert false + | _ -> `FunctionName ;; -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 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 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 - 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 pp_ref status ref = + capitalize (classify_reference status ref) + (NCicPp.r2s status true ref) -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 +(* cons avoid duplicates *) +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 ;; -exception DoNotExtract;; +let (@::) x l = let x,l = x @::: l in x::l;; -let pp_abstracted_ty current_module_uri = - let rec args context = +let rec pretty_print_type status ctxt = 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") + | Var n -> List.nth ctxt (n-1) + | Unit -> "()" + | Top -> assert false (* ??? *) + | 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 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 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 + match obj_kind with + TypeDeclaration (ctx,_) -> + (* data?? unsure semantics: inductive type without constructor, but + not matchable apparently *) + 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 + 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) -> + 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 = 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 -> + 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 ppobj current_module_uri obj = - let res = ppobj current_module_uri obj in - if res = "" then "" else res ^ ";;\n\n" -;; -*) -*) +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"