X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=993efe42cc4126f81f3c52e1cd9d633a07251f9b;hb=b4996474adbb67dda2e40b2bbcc727807fb48a1c;hp=32f5bc35e6fd28cfcf6a4318268cd922c3607d59;hpb=01dd8b3dcbf02a9645152496d64f649afbbd22b9;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 32f5bc35e..993efe42c 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -63,7 +63,7 @@ type typ = | Top | TConst of typformerreference | Arrow of typ * typ - | Skip of typ + | TSkip of typ | Forall of string * kind * typ | TAppl of typ list @@ -73,10 +73,10 @@ let rec size_of_type = | 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 + | Arrow _ -> 2 + | TSkip t -> size_of_type t + | Forall _ -> 2 + | TAppl l -> 1 ;; type term = @@ -87,8 +87,11 @@ type term = | Appl of term list | LetIn of string * (* typ **) term * term | Match of reference * term * term list + | BottomElim | TLambda of (* string **) term | Inst of (*typ_former **) term + | Skip of term + | UnsafeCoerce of term ;; let rec size_of_term = @@ -100,8 +103,11 @@ let rec size_of_term = | 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 + | 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)));; @@ -121,10 +127,15 @@ type obj_kind = | TypeDefinition of typ_former_def | TermDeclaration of term_former_decl | TermDefinition of term_former_def - | LetRec of obj_kind list - | Algebraic of (string * typ_context * (string * typ) list) list + | LetRec of (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 + +(* 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 context t = match NCicReduction.whd status ~subst:[] context t with @@ -282,7 +293,7 @@ let rec split_typ_prods context = function | Arrow (so,ta)-> split_typ_prods (Some ("_",`OfType so)::context) ta | Forall (name,so,ta)-> split_typ_prods (Some (name,`OfKind so)::context) ta - | Skip ta -> split_typ_prods (None::context) ta + | TSkip ta -> split_typ_prods (None::context) ta | _ as t -> context,t ;; @@ -291,7 +302,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 = @@ -351,7 +362,7 @@ let rec typ_of status ~metasenv context k = typ_of status ~metasenv ((b,NCic.Decl s)::context) t) | `PropKind | `Proposition -> - Skip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t) + TSkip (typ_of status ~metasenv ((b,NCic.Decl s)::context) t) | `Term _ -> assert false (* IMPOSSIBLE *)) | NCic.Sort _ | NCic.Implicit _ @@ -381,7 +392,7 @@ let rec fomega_subst k t1 = | TConst ref -> TConst ref | Unit -> Unit | Arrow (ty1,ty2) -> Arrow (fomega_subst k t1 ty1, fomega_subst (k+1) t1 ty2) - | Skip t -> Skip (fomega_subst (k+1) t1 t) + | TSkip t -> TSkip (fomega_subst (k+1) t1 t) | Forall (n,kind,t) -> Forall (n,kind,fomega_subst (k+1) t1 t) | TAppl args -> TAppl (List.map (fomega_subst k t1) args) @@ -415,7 +426,7 @@ let rec term_of status ~metasenv context = | `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 @@ -458,8 +469,22 @@ let rec term_of status ~metasenv context = 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) + (match classify_not_term status [] (NCic.Const ref) with + | `PropKind + | `KindOrType + | `Kind -> assert false (* IMPOSSIBLE *) + | `Proposition -> + (match pl with + [] -> BottomElim + | [p] -> + (* UnsafeCoerce not always required *) + UnsafeCoerce + (term_of status ~metasenv context p (* Lambdas will be skipped *)) + | _ -> assert false) + | `Type -> + Match (ref,term_of status ~metasenv context t, + (* UnsafeCoerce not always required *) + List.map (fun p -> UnsafeCoerce (term_of status ~metasenv context p)) pl)) and eat_args status metasenv acc context tyhe = function [] -> acc @@ -479,7 +504,7 @@ and eat_args status metasenv acc context tyhe = | Forall (_,_,t) -> eat_args status metasenv (Inst acc) context (fomega_subst 1 (typ_of status ~metasenv context arg) t) tl - | Skip t -> + | TSkip t -> eat_args status metasenv acc context t tl | Top -> assert false (*TODO: HOW??*) | Unit | Var _ | TConst _ | TAppl _ -> assert false (* NOT A PRODUCT *) @@ -492,7 +517,7 @@ type 'a result = | Success of 'a ;; -let object_of_constant status ~metasenv uri height bo ty = +let object_of_constant status ~metasenv ref bo ty = match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in @@ -510,14 +535,11 @@ let object_of_constant status ~metasenv uri height bo ty = String.uncapitalize (fst n),k) p1) ctx0 ctx in - (* BUG here: for mutual type definitions the spec is not good *) - let ref = - NReference.reference_of_spec uri (NReference.Def height) in let bo = typ_of status ~metasenv ctx bo in status#set_extraction_db (ReferenceMap.add ref (nicectx,Some bo) status#extraction_db), - Success (uri,TypeDefinition((nicectx,res),bo)) + Success (ref,TypeDefinition((nicectx,res),bo)) | `Kind -> status, Erased (* DPM: but not really, more a failure! *) | `PropKind | `Proposition -> status, Erased @@ -529,14 +551,14 @@ let object_of_constant status ~metasenv uri height bo ty = (* CSC: TO BE FINISHED, REF NON REGISTERED *) let ty = typ_of status ~metasenv [] ty in status, - Success (uri, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo)) + Success (ref, TermDefinition (split_typ_prods [] ty, term_of status ~metasenv [] bo)) | `Term _ -> status, Failure "Non-term classified as a term. This is a bug." ;; let object_of_inductive status ~metasenv uri ind leftno il = let status,_,rev_tyl = List.fold_left - (fun (status,i,res) (_,name,arity,cl) -> + (fun (status,i,res) (_,_,arity,cl) -> match classify_not_term status [] arity with | `Proposition | `KindOrType @@ -545,58 +567,68 @@ let object_of_inductive status ~metasenv uri ind leftno il = | `Kind -> let arity = kind_of status ~metasenv [] arity in let ctx,_ = split_kind_prods [] arity in + let right,left = HExtlib.split_nth (List.length ctx - leftno) ctx in let ref = NReference.reference_of_spec uri (NReference.Ind (ind,i,leftno)) in let status = status#set_extraction_db (ReferenceMap.add ref (ctx,None) status#extraction_db) in let cl = - List.map - (fun (_,name,ty) -> + HExtlib.list_mapi + (fun (_,_,ty) j -> let ctx,ty = NCicReduction.split_prods status ~subst:[] [] leftno ty in let ty = typ_of status ~metasenv ctx ty in - name,ty + NReference.mk_constructor (j+1) ref,ty ) cl in - status,i+1,(name,ctx,cl)::res + status,i+1,(ref,left,right,cl)::res ) (status,0,[]) il in match rev_tyl with [] -> status,Erased - | _ -> status, Success (uri, Algebraic (List.rev rev_tyl)) + | _ -> status, Success (dummyref, Algebraic (List.rev rev_tyl)) ;; let object_of status (uri,height,metasenv,subst,obj_kind) = let obj_kind = apply_subst subst obj_kind in match obj_kind with | NCic.Constant (_,_,None,ty,_) -> + let ref = NReference.reference_of_spec uri NReference.Decl in (match classify status ~metasenv [] ty with | `Kind -> let ty = kind_of status ~metasenv [] ty in let ctx,_ as res = split_kind_prods [] ty in - let ref = NReference.reference_of_spec uri NReference.Decl in status#set_extraction_db - (ReferenceMap.add ref (ctx,None) status#extraction_db), Success (uri, TypeDeclaration res) + (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 (uri, TermDeclaration (split_typ_prods [] ty)) + status, Success (ref, TermDeclaration (split_typ_prods [] ty)) | `Term _ -> status, Failure "Type classified as a term. This is a bug.") | NCic.Constant (_,_,Some bo,ty,_) -> - object_of_constant status ~metasenv uri height bo ty - | NCic.Fixpoint (_fix_or_cofix,fs,_) -> - let status,objs = + let ref = NReference.reference_of_spec uri (NReference.Def height) in + object_of_constant status ~metasenv ref bo ty + | NCic.Fixpoint (fix_or_cofix,fs,_) -> + let _,status,objs = List.fold_right - (fun (_,_name,_,ty,bo) (status,res) -> - let status,obj = object_of_constant ~metasenv status uri height bo ty in + (fun (_,_name,recno,ty,bo) (i,status,res) -> + let ref = + if fix_or_cofix then + NReference.reference_of_spec + uri (NReference.Fix (i,recno,height)) + else + NReference.reference_of_spec uri (NReference.CoFix i) + in + let status,obj = object_of_constant ~metasenv status ref bo ty in match obj with - | Success (_uri,obj) -> status, obj::res - | _ -> status, res) fs (status,[]) + | Success (ref,obj) -> i+1,status, (ref,obj)::res + | _ -> i+1,status, res) fs (0,status,[]) in - status, Success (uri,LetRec objs) + status, Success (dummyref,LetRec objs) | NCic.Inductive (ind,leftno,il,_) -> object_of_inductive status ~metasenv uri ind leftno il @@ -690,22 +722,25 @@ let classify_reference status ref = if ReferenceMap.mem ref status#extraction_db then `TypeName else - `FunctionName + let NReference.Ref (_,ref) = ref in + match ref with + NReference.Con _ -> `Constructor + | NReference.Ind _ -> assert false + | _ -> `FunctionName ;; let capitalize classification name = match classification with | `Constructor | `TypeName -> idiomatic_haskell_type_name_of_string name + | `TypeVariable + | `BoundVariable | `FunctionName -> idiomatic_haskell_term_name_of_string name ;; let pp_ref status ref = capitalize (classify_reference status ref) - (NCicPp.r2s status false ref) - -let name_of_uri classification uri = - capitalize classification (NUri.name_of_uri uri) + (NCicPp.r2s status true ref) (* cons avoid duplicates *) let rec (@:::) name l = @@ -728,14 +763,15 @@ let rec pretty_print_type status ctxt = | Arrow (t1,t2) -> bracket size_of_type (pretty_print_type status ctxt) t1 ^ " -> " ^ pretty_print_type status ("_"::ctxt) t2 - | Skip t -> pretty_print_type status ("_"::ctxt) t + | TSkip t -> pretty_print_type status ("_"::ctxt) t | Forall (name, kind, t) -> (*CSC: BUG HERE: avoid clashes due to uncapitalisation*) - let name = String.uncapitalize name in + let name = capitalize `TypeVariable name in + let name,ctxt = name@:::ctxt in if size_of_kind kind > 1 then - "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name@::ctxt) t + "forall (" ^ name ^ " :: " ^ pretty_print_kind kind ^ "). " ^ pretty_print_type status (name::ctxt) t else - "forall " ^ name ^ ". " ^ pretty_print_type status (name@::ctxt) t + "forall " ^ name ^ ". " ^ pretty_print_type status (name::ctxt) t | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) let rec pretty_print_term status ctxt = @@ -743,10 +779,20 @@ let rec pretty_print_term status ctxt = | Rel n -> List.nth ctxt (n-1) | UnitTerm -> "()" | Const ref -> pp_ref status ref - | Lambda (name,t) -> "\\" ^ name ^ " -> " ^ pretty_print_term status (name@::ctxt) t + | Lambda (name,t) -> + let name = capitalize `BoundVariable name in + let name,ctxt = name@:::ctxt in + "\\" ^ name ^ " -> " ^ pretty_print_term status (name::ctxt) t | Appl tl -> String.concat " " (List.map (bracket size_of_term (pretty_print_term status ctxt)) tl) | LetIn (name,s,t) -> - "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ pretty_print_term status (name@::ctxt) t + let name = capitalize `BoundVariable name in + let name,ctxt = name@:::ctxt in + "let " ^ name ^ " = " ^ pretty_print_term status ctxt s ^ " in " ^ + pretty_print_term status (name::ctxt) t + | BottomElim -> + "error \"Unreachable code\"" + | UnsafeCoerce t -> + "unsafeCoerce " ^ bracket size_of_term (pretty_print_term status ctxt) t | Match (r,matched,pl) -> if pl = [] then "error \"Case analysis over empty type\"" @@ -783,7 +829,8 @@ let rec pretty_print_term status ctxt = in " " ^ pattern ^ " -> " ^ body ) patterns) - | TLambda t -> pretty_print_term status ctxt t + | Skip t + | TLambda t -> pretty_print_term status (""@::ctxt) t | Inst t -> pretty_print_term status ctxt t ;; @@ -794,17 +841,17 @@ type term_former_def = term_context * term * typ type term_former_decl = term_context * typ *) -let rec pp_obj status (uri,obj_kind) = +let rec pp_obj status (ref,obj_kind) = let pretty_print_context ctx = - String.concat " " (List.rev + String.concat " " (List.rev (snd (List.fold_right - (fun (x,kind) l -> + (fun (x,kind) (l,res) -> let x,l = x @:::l in if size_of_kind kind > 1 then - ("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::l + x::l,("(" ^ x ^ " :: " ^ pretty_print_kind kind ^ ")")::res else - x::l) - (HExtlib.filter_map (fun x -> x) ctx) [])) + x::l,x::res) + (HExtlib.filter_map (fun x -> x) ctx) ([],[])))) in let namectx_of_ctx ctx = List.fold_right (@::) @@ -814,38 +861,37 @@ let rec pp_obj status (uri,obj_kind) = (* data?? unsure semantics: inductive type without constructor, but not matchable apparently *) if List.length ctx = 0 then - "data " ^ name_of_uri `TypeName uri + "data " ^ pp_ref status ref else - "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx + "data " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx | TypeDefinition ((ctx, _),ty) -> let namectx = namectx_of_ctx ctx in if List.length ctx = 0 then - "type " ^ name_of_uri `TypeName uri ^ " = " ^ pretty_print_type status namectx ty + "type " ^ pp_ref status ref ^ " = " ^ pretty_print_type status namectx ty else - "type " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty + "type " ^ pp_ref status ref ^ " " ^ pretty_print_context ctx ^ " = " ^ pretty_print_type status namectx ty | TermDeclaration (ctx,ty) -> - let name = name_of_uri `FunctionName uri in + let name = pp_ref status ref in name ^ " :: " ^ pretty_print_type status [] (glue_ctx_typ ctx ty) ^ "\n" ^ name ^ " = error \"The declaration `" ^ name ^ "' has yet to be defined.\"" | TermDefinition ((ctx,ty),bo) -> - let name = name_of_uri `FunctionName uri in + let name = pp_ref status ref in let namectx = namectx_of_ctx ctx in (*CSC: BUG here *) name ^ " :: " ^ pretty_print_type status namectx (glue_ctx_typ ctx ty) ^ "\n" ^ name ^ " = " ^ pretty_print_term status namectx bo | LetRec l -> - (*CSC: BUG always uses the name of the URI *) - String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) l) + String.concat "\n" (List.map (pp_obj status) l) | Algebraic il -> String.concat "\n" (List.map - (fun _name,ctx,cl -> - (*CSC: BUG always uses the name of the URI *) - "data " ^ name_of_uri `TypeName uri ^ " " ^ pretty_print_context ctx ^ " where\n " ^ + (fun ref,left,right,cl -> + "data " ^ pp_ref status ref ^ " " ^ + pretty_print_context (right@left) ^ " where\n " ^ String.concat "\n " (List.map - (fun name,tys -> - let namectx = namectx_of_ctx ctx in - capitalize `Constructor name ^ " :: " ^ + (fun ref,tys -> + let namectx = namectx_of_ctx left in + pp_ref status ref ^ " :: " ^ pretty_print_type status namectx tys ) cl )) il)