X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=7b24f74c0c741b799f29dd6d95f7318bd1eac82f;hb=87e64004d2fb44077b68c4f9c009223b81ad2b6d;hp=afe79e7af62c3966ccd1282b8de0b0ef889ffc91;hpb=efdc4b8deed29fbcd4b2673e1f174696cd4c67d6;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index afe79e7af..7b24f74c0 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -95,7 +95,7 @@ type term = | LetIn of string * (* typ **) term * term | Match of reference * term * (term_context * term) list | BottomElim - | TLambda of (* string **) term + | TLambda of string * term | Inst of (*typ_former **) term | Skip of term | UnsafeCoerce of term @@ -104,17 +104,22 @@ type 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 (name, body) -> 1 + size_of_term body + | Lambda (_, 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 + | 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 + | 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 @@ -331,7 +336,9 @@ let context_of_typformer status ~metasenv context = | NCic.Const (NReference.Ref (_,NReference.Fix _) as ref) -> (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 = @@ -419,7 +426,7 @@ 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) @@ -450,21 +457,10 @@ let rec term_of status ~metasenv context = | NCic.Appl (he::args) -> eat_args status metasenv (term_of status ~metasenv context he) context + (*BUG: recomputing every time the type of the head*) (typ_of status ~metasenv context (NCicTypeChecker.typeof status ~metasenv ~subst:[] context he)) args -(* - let he_context = context_of_typformer status ~metasenv context he in - let process_args he = - function - `Empty -> he - | `Inst tl -> Inst (process_args he tl) - | `Appl (arg,tl) -> process_args (Appl (he,... arg)) tl - in - Appl (typ_of status ~metasenv context he :: - process_args (typ_of status ~metasenv context he) - (skip_term_args status ~metasenv context (List.rev he_context,args)) -*) | NCic.Appl _ -> assert false (* TODO: when head is a match/let rec; otherwise NOT A TYPE *) | NCic.Meta _ -> assert false (* TODO *) @@ -477,20 +473,35 @@ let rec term_of status ~metasenv context = in let rec eat_branch n ty context ctx pat = match (ty, pat) with - | NCic.Prod (_, _, t), _ when n > 0 -> + | TSkip t,_ + | Forall (_,_,t),_ + | Arrow (_, t), _ when n > 0 -> eat_branch (pred n) t context ctx pat - | NCic.Prod (_, _, t), NCic.Lambda (name, ty, t') -> + | _, _ 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 = - (*BUG: we should classify according to the constructor type*) - (Some (name,`OfType (*(typ_of status ~metasenv context ty)*)Unit))::ctx in + (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 *) @@ -515,11 +526,6 @@ and eat_args status metasenv acc context tyhe = function [] -> acc | arg::tl -> - let mk_appl f x = - match f with - Appl args -> Appl (args@[x]) - | _ -> Appl [f;x] - in match fomega_whd status tyhe with Arrow (s,t) -> let arg = @@ -801,18 +807,18 @@ let rec pretty_print_type status ctxt = | TAppl tl -> String.concat " " (List.map (pretty_print_type status ctxt) tl) let pretty_print_term_context status ctx1 ctx2 = - let name_context, res = + let name_context, rev_res = List.fold_right - (fun el (ctx1,res) -> + (fun el (ctx1,rev_res) -> match el with - None -> ""@::ctx1,res - | Some (name,`OfKind _) -> name@::ctx1,res + 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 ^ ")")::res + ("(" ^ name ^ " :: " ^ pretty_print_type status ctx1 typ ^ ")")::rev_res ) ctx2 (ctx1,[]) in - name_context, String.concat " " res + name_context, String.concat " " (List.rev rev_res) let rec pretty_print_term status ctxt = function @@ -843,15 +849,17 @@ let rec pretty_print_term status ctxt = (fun (bound_names,rhs) i -> let ref = NReference.mk_constructor (i+1) r in let name = pp_ref status ref in - let names,bound_names = + let ctxt,bound_names = pretty_print_term_context status ctxt bound_names in let body = - pretty_print_term status ((List.rev names)@ctxt) rhs + pretty_print_term status ctxt rhs in " " ^ name ^ " " ^ bound_names ^ " -> " ^ body ) pl) - | Skip t - | TLambda t -> pretty_print_term status (""@::ctxt) t + | 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 ;;