From 9a63ba27eb9b9b78b2745c85828416de316c063f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 27 Aug 2012 08:58:57 +0000 Subject: [PATCH] 1. Dominic: - kinds signature in explicit for-all (if not simple kinds) - Haskell names of Matita names (still bugged) - improved pretty-printing (only necessary brackets) 2. CC types are now extracted to F_omega types even when NotInFOmega (exception removed altogether) --- matita/components/ng_kernel/nCicExtraction.ml | 1411 ++++------------- 1 file changed, 308 insertions(+), 1103 deletions(-) diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 8b8a7b216..cbcc24c24 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -32,31 +32,77 @@ 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 *) + +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 +;; + +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 - | Skip of typ - | Forall of string * kind * typ - | TAppl of typ list + | 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_type = + function + | Var v -> 1 + | Unit -> 1 + | Top -> 1 + | TConst c -> 1 + | Arrow (l, r) -> 1 + size_of_type l + size_of_type r + | Skip t -> size_of_type t + | Forall (name, kind, typ) -> 1 + size_of_type typ + | TAppl l -> List.fold_right (+) (List.map size_of_type l) 0 +;; 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 + | 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 rec size_of_term = + function + | Rel r -> 1 + | UnitTerm -> 1 + | Const c -> 1 + | Lambda (name, body) -> 1 + size_of_term body + | Appl l -> List.length l + | LetIn (name, def, body) -> 1 + size_of_term def + size_of_term body + | Match (name, case, pats) -> 1 + size_of_term case + List.length pats + | TLambda t -> size_of_term t + | Inst t -> 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)));; @@ -80,23 +126,17 @@ type obj_kind = type obj = NUri.uri * obj_kind -exception NotInFOmega - -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 _ @@ -107,7 +147,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 @@ -130,7 +170,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 +179,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 *) @@ -155,11 +195,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 @@ -173,13 +213,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) @@ -317,7 +356,7 @@ let rec typ_of status ~metasenv context k = | 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) -> @@ -446,7 +485,14 @@ and eat_args status metasenv acc context tyhe = | 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 uri height bo ty = match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in @@ -471,28 +517,27 @@ let obj_of_constant status ~metasenv uri height bo ty = status#set_extraction_db (ReferenceMap.add ref (nicectx,Some bo) status#extraction_db), - Some (uri,TypeDefinition((nicectx,res),bo)) - | `Kind -> status, None + Success (uri,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 (uri, 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_inductive status ~metasenv uri ind leftno il = +let object_of_inductive status ~metasenv uri ind leftno il = let tyl = HExtlib.filter_map (fun _,name,arity,cl -> - match classify_not_term status true [] arity with + match classify_not_term status [] arity with | `Proposition | `KindOrType | `Type -> assert false (* IMPOSSIBLE *) @@ -508,62 +553,141 @@ let obj_of_inductive status ~metasenv uri ind leftno il = | _ -> status, Some (uri, Algebraic tyl) ;; -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 (ind,leftno,il,_) -> - obj_of_inductive status ~metasenv uri ind leftno il - with - NotInFOmega -> - prerr_endline "-- NOT IN F_omega"; - status, None +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,_) -> + (match classify status ~metasenv [] ty with + | `Kind -> + let ty = kind_of status ~metasenv [] ty in + let ctx,_ as res = split_kind_prods [] ty in + let ref = NReference.reference_of_spec uri NReference.Decl in + status#set_extraction_db + (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res) + | `PropKind + | `Proposition -> status, Erased + | `Type + | `KindOrType (*???*) -> + let ty = typ_of status ~metasenv [] ty in + status, Success (uri, TermDeclaration (split_typ_prods [] ty)) + | `Term _ -> status, Failure "Type classified as a term. This is a bug.") + | NCic.Constant (_,_,Some bo,ty,_) -> + object_of_constant status ~metasenv uri height bo ty + | NCic.Fixpoint (_fix_or_cofix,fs,_) -> + let status,objs = + List.fold_right + (fun (_,_name,_,ty,bo) (status,res) -> + let status,obj = object_of_constant ~metasenv status uri height bo ty in + match obj with + | Success (_uri,obj) -> status, obj::res + | _ -> status, res) fs (status,[]) + in + status, Success (uri,LetRec objs) + | NCic.Inductive (ind,leftno,il,_) -> + let status, obj_of_inductive = object_of_inductive status ~metasenv uri ind leftno il in + match obj_of_inductive with + | None -> status, Failure "Could not extract an inductive type." + | Some s -> status, Success s (************************ 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 + `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 + | `FunctionName -> idiomatic_haskell_term_name_of_string name +;; let pp_ref status ref = capitalize (classify_reference status ref) @@ -582,75 +706,70 @@ let rec (@::) 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 +let rec pretty_print_type status ctxt = + function + | 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 + | Skip t -> pretty_print_type status ("_"::ctxt) t + | Forall (name, kind, t) -> + (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) + let name = String.uncapitalize name in + 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 rec pretty_print_term status ctxt = + function + | Rel n -> List.nth ctxt (n-1) + | UnitTerm -> "()" + | Const ref -> pp_ref status ref + | Lambda (name,t) -> "\\" ^ name ^ " -> " ^ pretty_print_term status (name@::ctxt) t + | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl) + | LetIn (name,s,t) -> + "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t + | 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 - " " ^ pattern ^ " -> " ^ body - ) patterns) - | TLambda t -> pp_term status ctx t - | Inst t -> pp_term status ctx t + let j = ref 0 in + let patterns = + try + List.map2 + (fun (_, name, ty) pat -> incr j; name, eat_branch leftno ty pat) constructors pl + with Invalid_argument _ -> assert false + in + "case " ^ pretty_print_term status ctxt matched ^ " of\n" ^ + String.concat "\n" + (List.map + (fun (name,(bound_names,rhs)) -> + let pattern,body = + (*CSC: BUG avoid name clashes *) + String.concat " " (String.capitalize name::bound_names), + pretty_print_term status ((List.rev bound_names)@ctxt) rhs + in + " " ^ pattern ^ " -> " ^ body + ) patterns) + | TLambda t -> pretty_print_term status ctxt t + | Inst t -> pretty_print_term status ctxt t +;; (* type term_context = (string * [`OfKind of kind | `OfType of typ]) option list @@ -660,10 +779,11 @@ type term_former_decl = term_context * typ *) 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 pretty_print_context ctx = + String.concat " " (List.rev + (List.fold_right (fun (x,kind) 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 @@ -671,22 +791,26 @@ 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 " ^ name_of_uri `TypeName uri + else + "data " ^ name_of_uri `TypeName uri ^ " " ^ 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 " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty + else + "type " ^ name_of_uri `TypeName uri ^ " " ^ 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" + 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 namectx = namectx_of_ctx ctx in (*CSC: BUG here *) - name ^ " :: " ^ pp_typ status ["a";"b";"c"] (glue_ctx_typ ctx ty) ^ "\n" ^ - name ^ " = " ^ pp_term status namectx bo + 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) @@ -695,939 +819,20 @@ let rec pp_obj status (uri,obj_kind) = (List.map (fun _name,ctx,cl -> (*CSC: BUG always uses the name of the URI *) - "data " ^ name_of_uri `TypeName uri ^ " " ^ pp_ctx ctx ^ " = " ^ + "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ String.concat " | " (List.map (fun name,tys -> capitalize `Constructor name ^ - String.concat " " (List.map (pp_typ status []) tys) + String.concat " " (List.map (pretty_print_type status []) tys) ) cl )) il) (* inductive and records missing *) let haskell_of_obj status obj = - let status, obj = obj_of status obj in + let status, obj = object_of status obj in status, match obj with - None -> "-- ERASED\n" - | Some obj -> pp_obj status obj ^ "\n" - -(* -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 = - 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 -;; - -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 - 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" -;; -*) -*) + Erased -> "-- [?] Erased due to term being propositionally irrelevant.\n" + | OutsideTheory -> "-- [?] Erased due to image of term under extraction residing outside Fω.\n" + | Failure msg -> "-- [!] FAILURE: " ^ msg ^ "\n" + | Success o -> pp_obj status o ^ "\n" -- 2.39.2