X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fcomponents%2Fng_kernel%2FnCicExtraction.ml;h=7b24f74c0c741b799f29dd6d95f7318bd1eac82f;hb=87e64004d2fb44077b68c4f9c009223b81ad2b6d;hp=993efe42cc4126f81f3c52e1cd9d633a07251f9b;hpb=b4996474adbb67dda2e40b2bbcc727807fb48a1c;p=helm.git diff --git a/matita/components/ng_kernel/nCicExtraction.ml b/matita/components/ng_kernel/nCicExtraction.ml index 993efe42c..7b24f74c0 100644 --- a/matita/components/ng_kernel/nCicExtraction.ml +++ b/matita/components/ng_kernel/nCicExtraction.ml @@ -79,6 +79,13 @@ let rec size_of_type = | TAppl l -> 1 ;; +(* None = dropped abstraction *) +type typ_context = (string * kind) option list +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 @@ -86,25 +93,33 @@ type term = | Lambda of string * (* typ **) term | Appl of term list | LetIn of string * (* typ **) term * term - | Match of reference * term * term list + | 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 ;; +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 @@ -112,16 +127,6 @@ let rec size_of_term = let unitty = NCic.Const (NReference.reference_of_spec (NUri.uri_of_string "cic:/matita/basics/types/unit.ind") (NReference.Ind (true,0,0)));; -(* None = dropped abstraction *) -type typ_context = (string * kind) option list -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_former_decl = term_context * typ -type term_former_def = term_former_decl * term - type obj_kind = TypeDeclaration of typ_former_decl | TypeDefinition of typ_former_def @@ -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,50 +457,75 @@ 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 *) | NCic.Match (ref,_,t,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 pl with + (match patterns_of pl with [] -> BottomElim - | [p] -> - (* UnsafeCoerce not always required *) - UnsafeCoerce - (term_of status ~metasenv context p (* Lambdas will be skipped *)) + | [_lhs,rhs] -> rhs (*BUG HERE: Rels are not ok, bound in the _lhs*) | _ -> 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)) + Match (ref,term_of status ~metasenv context t, patterns_of pl)) 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 = @@ -774,6 +806,20 @@ let rec pretty_print_type status ctxt = "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) @@ -797,50 +843,26 @@ let rec pretty_print_term status ctxt = if pl = [] then "error \"Case analysis over empty type\"" else - 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 " ^ 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) - | Skip t - | TLambda t -> pretty_print_term status (""@::ctxt) t + "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 ;; -(* -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 rec pp_obj status (ref,obj_kind) = let pretty_print_context ctx = String.concat " " (List.rev (snd