X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=8b8a7b216c74e360238b183789ed2acdb3319c6c;hb=933f288c1ef283f50050ce51fbe6773f25fc68ea;hp=3f950aa40d269c3026851f7d66ec4d15c2ff4848;hpb=08773d437c210a2da1f1f481b7efc25727c0e0ca;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 3f950aa40..8b8a7b216 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -75,8 +75,8 @@ type obj_kind = | 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 obj_kind list + | Algebraic of (string * typ_context * (string * typ list) list) list type obj = NUri.uri * obj_kind @@ -446,6 +446,68 @@ 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 = + 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 + (* 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), + Some (uri,TypeDefinition((nicectx,res),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 *) +;; + +let obj_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 + | `Proposition + | `KindOrType + | `Type -> assert false (* IMPOSSIBLE *) + | `PropKind -> None + | `Kind -> + let arity = kind_of status ~metasenv [] arity in + let ctx,_ as res = split_kind_prods [] arity in + Some (name,ctx,[]) + ) il + in + match tyl with + [] -> status,None + | _ -> 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 @@ -468,44 +530,20 @@ let obj_of status (uri,height,metasenv,subst,obj_kind) = 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 - let bo = typ_of status ~metasenv ctx bo in - status#set_extraction_db - (ReferenceMap.add ref (nicectx,Some bo) - status#extraction_db), - Some (uri,TypeDefinition((nicectx,res),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 *)) + 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"; @@ -574,7 +612,43 @@ let rec pp_term status ctx = | 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 *) + | Match (r,matched,pl) -> + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys status r in + let _,_,_,cl = List.nth tys n in + cl,leftno + in + let rec eat_branch n ty pat = + match (ty, pat) with + | NCic.Prod (_, _, t), _ when n > 0 -> + eat_branch (pred n) t pat + | NCic.Prod (_, _, t), Lambda (name, t') -> + (*CSC: BUG HERE; WHAT IF SOME ARGUMENTS ARE DELETED?*) + let cv, rhs = eat_branch 0 t t' in + name :: cv, rhs + | _, _ -> [], pat + in + let j = ref 0 in + let patterns = + try + List.map2 + (fun (_, name, ty) pat -> + incr j; + name, eat_branch leftno ty pat + ) constructors pl + with Invalid_argument _ -> assert false + in + "case " ^ pp_term status ctx matched ^ " of\n" ^ + String.concat "\n" + (List.map + (fun (name,(bound_names,rhs)) -> + let pattern,body = + (*CSC: BUG avoid name clashes *) + String.concat " " (String.capitalize name::bound_names), + pp_term status ((List.rev bound_names)@ctx) rhs + in + " " ^ pattern ^ " -> " ^ body + ) patterns) | TLambda t -> pp_term status ctx t | Inst t -> pp_term status ctx t @@ -585,7 +659,7 @@ type term_former_def = term_context * term * typ type term_former_decl = term_context * typ *) -let pp_obj status (uri,obj_kind) = +let rec pp_obj status (uri,obj_kind) = let pp_ctx ctx = String.concat " " (List.rev (List.fold_right (fun (x,_) l -> x@::l) @@ -610,10 +684,25 @@ let pp_obj status (uri,obj_kind) = | 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 - | LetRec _ -> assert false (* TODO - (* inductive and records missing *)*) + | LetRec l -> + (*CSC: BUG always uses the name of the URI *) + String.concat "\n" (List.map (fun obj -> pp_obj status (uri,obj)) 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 ^ " " ^ pp_ctx ctx ^ " = " ^ + String.concat " | " (List.map + (fun name,tys -> + capitalize `Constructor name ^ + String.concat " " (List.map (pp_typ status []) tys) + ) cl + )) il) + (* inductive and records missing *) let haskell_of_obj status obj = let status, obj = obj_of status obj in