From: Claudio Sacerdoti Coen Date: Sun, 12 Apr 2009 10:56:31 +0000 (+0000) Subject: Match is now rendered as best as possible. X-Git-Tag: make_still_working~4089 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7deb0d8f534f779adb1b5813a7f159609b9cba3c;hp=6abf435197c2bc37fadc0b3bd5925cd9cbe112e2;p=helm.git Match is now rendered as best as possible. --- diff --git a/helm/software/components/ng_cic_content/nTermCicContent.ml b/helm/software/components/ng_cic_content/nTermCicContent.ml index b3c827f92..826238d1c 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.ml +++ b/helm/software/components/ng_cic_content/nTermCicContent.ml @@ -45,35 +45,12 @@ type term_info = let get_types uri = let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in match o with - | Cic.InductiveDefinition (l,_,lpsno,_) -> l, lpsno + | Cic.InductiveDefinition (l,_,leftno,_) -> l, leftno | _ -> assert false - -let name_of_inductive_type uri i = - let types, _ = get_types uri in - let (name, _, _, _) = try List.nth types i with Not_found -> assert false in - name - - (* returns pairs *) -let constructors_of_inductive_type uri i = - let types, _ = get_types uri in - let (_, _, _, constructors) = - try List.nth types i with Not_found -> assert false - in - constructors - - (* returns name only *) -let constructor_of_inductive_type uri i j = - (try - fst (List.nth (constructors_of_inductive_type uri i) (j-1)) - with Not_found -> assert false) - - (* returns the number of left parameters *) -let left_params_no_of_inductive_type uri = - snd (get_types uri) *) (* CODICE c&p da NCicPp *) -let nast_of_cic ~subst ~context = +let nast_of_cic ~output_type ~subst ~context = let rec k ctx = function | NCic.Rel n -> (try @@ -124,38 +101,44 @@ let nast_of_cic ~subst ~context = | NCic.Appl l -> NCic.Appl (l@args) | _ -> NCic.Appl (hd :: args))) | NCic.Appl args -> Ast.Appl (List.map (k ctx) args) - | NCic.Match (uri,ty,te,patterns) -> -(* - let name = NReference.name_of_reference uri in + | NCic.Match (NReference.Ref (uri,_) as r,outty,te,patterns) -> + let name = NUri.name_of_uri uri in +(* CSC let uri_str = UriManager.string_of_uri uri in let puri_str = sprintf "%s#xpointer(1/%d)" uri_str (typeno+1) in let ctor_puri j = UriManager.uri_of_string (sprintf "%s#xpointer(1/%d/%d)" uri_str (typeno+1) j) in - let case_indty = name, Some (UriManager.uri_of_string puri_str) in - let constructors = constructors_of_inductive_type uri typeno in - let lpsno = left_params_no_of_inductive_type uri in - let rec eat_branch n ty pat = +*) + let case_indty = + name, None(*CSC Some (UriManager.uri_of_string puri_str)*) in + let constructors, leftno = + let _,leftno,tys,_,n = NCicEnvironment.get_checked_indtys r in + let _,_,_,cl = List.nth tys n in + cl,leftno + in + let rec eat_branch n ctx ty pat = match (ty, pat) with - | NCic.Prod (_, _, t), _ when n > 0 -> eat_branch (pred n) t pat - | NCic.Prod (_, _, t), NCic.ALambda (_, name, s, t') -> - let (cv, rhs) = eat_branch 0 t t' in - (CicNotationUtil.name_of_cic_name name, Some (k s)) :: cv, rhs - | _, _ -> [], k pat + | NCic.Prod (name, s, t), _ when n > 0 -> + eat_branch (pred n) ((name,NCic.Decl s)::ctx) t pat + | NCic.Prod (_, _, t), NCic.Lambda (name, s, t') -> + let cv, rhs = eat_branch 0 ((name,NCic.Decl s)::ctx) t t' in + (Ast.Ident (name,None), Some (k ctx s)) :: cv, rhs + | _, _ -> [], k ctx pat in let j = ref 0 in let patterns = try List.map2 - (fun (name, ty) pat -> + (fun (_, name, ty) pat -> incr j; let name,(capture_variables,rhs) = match output_type with - `Term -> name, eat_branch lpsno ty pat - | `Pattern -> "_", ([], k pat) + `Term -> name, eat_branch leftno ctx ty pat + | `Pattern -> "_", ([], k ctx pat) in - Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs + Ast.Pattern (name, None(*CSC Some (ctor_puri !j)*), capture_variables), rhs ) constructors patterns with Invalid_argument _ -> assert false in @@ -164,8 +147,7 @@ let nast_of_cic ~subst ~context = `Pattern -> None | `Term -> Some case_indty in - idref id (Ast.Case (k te, indty, Some (k ty), patterns)) -*) assert false + Ast.Case (k ctx te, indty, Some (k ctx outty), patterns) in k context ;; @@ -185,7 +167,7 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = K.dec_id = "-1"; K.dec_inductive = false; K.dec_aref = "-1"; - K.dec_type = nast_of_cic ~subst ~context t + K.dec_type = nast_of_cic ~output_type:`Term ~subst ~context t })::res,item::context | name,NCic.Def (t,ty) -> Some @@ -195,12 +177,12 @@ let nmap_sequent ~subst (i,(n,context,ty):int * NCic.conjecture) = { K.def_name = (Some name); K.def_id = "-1"; K.def_aref = "-1"; - K.def_term = nast_of_cic ~subst ~context t; - K.def_type = nast_of_cic ~subst ~context ty + K.def_term = nast_of_cic ~output_type:`Term ~subst ~context t; + K.def_type = nast_of_cic ~output_type:`Term ~subst ~context ty })::res,item::context ) context ([],[]) in - "-1",i,context',nast_of_cic ~subst ~context ty + "-1",i,context',nast_of_cic ~output_type:`Term ~subst ~context ty ;; (* diff --git a/helm/software/components/ng_cic_content/nTermCicContent.mli b/helm/software/components/ng_cic_content/nTermCicContent.mli index e66e2ef7a..fb6236553 100644 --- a/helm/software/components/ng_cic_content/nTermCicContent.mli +++ b/helm/software/components/ng_cic_content/nTermCicContent.mli @@ -76,7 +76,10 @@ val push: unit -> unit val pop: unit -> unit *) +(* val nast_of_cic : - subst:NCic.substitution -> context:NCic.context -> NCic.term -> - CicNotationPt.term + output_type:[`Pattern | `Term ] -> + subst:NCic.substitution -> context:NCic.context -> NCic.term -> + CicNotationPt.term +*) val nmap_sequent : subst:NCic.substitution -> int * NCic.conjecture -> CicNotationPt.term Content.conjecture