X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=89dba29879c05208045c4685cc2e6c3f0e92b319;hb=8c4659819a1c1f2e450d9a588ecca37d95ae48e9;hp=0f51e36a9acf9fb2241017a0a12580bdccb5a72d;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 0f51e36a9..89dba2987 100644 --- a/helm/software/components/content_pres/termContentPres.ml +++ b/helm/software/components/content_pres/termContentPres.ml @@ -42,18 +42,9 @@ let resolve_binder = function | `Forall -> "\\forall" | `Exists -> "\\exists" -let add_level_info prec assoc t = Ast.AttributedTerm (`Level (prec, assoc), t) -let add_pos_info pos t = Ast.AttributedTerm (`ChildPos pos, t) -let left_pos = add_pos_info `Left -let right_pos = add_pos_info `Right -let inner_pos = add_pos_info `Inner - -let rec top_pos t = add_level_info ~-1 Gramext.NonA (inner_pos t) -(* function - | Ast.AttributedTerm (`Level _, t) -> - add_level_info ~-1 Gramext.NonA (inner_pos t) - | Ast.AttributedTerm (attr, t) -> Ast.AttributedTerm (attr, top_pos t) - | t -> add_level_info ~-1 Gramext.NonA (inner_pos t) *) +let add_level_info prec t = Ast.AttributedTerm (`Level prec, t) + +let rec top_pos t = add_level_info ~-1 t let rec remove_level_info = function @@ -100,7 +91,7 @@ let binder_symbol s = let string_of_sort_kind = function | `Prop -> "Prop" | `Set -> "Set" - | `CProp -> "CProp" + | `CProp _ -> "CProp" | `Type _ -> "Type" let pp_ast0 t k = @@ -112,18 +103,18 @@ let pp_ast0 t k = | [] -> [] | [ last ] -> let last = k last in - if pos = `Left then [ left_pos last ] else [ right_pos last ] + [ last ] | hd :: tl -> - (add_pos_info pos (k hd)) :: aux_args `Inner tl + (k hd) :: aux_args `Inner tl in - add_level_info Ast.apply_prec Ast.apply_assoc + add_level_info Ast.apply_prec (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts))) | Ast.Binder (binder_kind, (id, ty), body) -> - add_level_info Ast.binder_prec Ast.binder_assoc + add_level_info Ast.binder_prec (hvbox false true [ binder_symbol (resolve_binder binder_kind); k id; builtin_symbol ":"; aux_ty ty; break; - builtin_symbol "."; right_pos (k body) ]) + builtin_symbol "."; k body ]) | Ast.Case (what, indty_opt, outty_opt, patterns) -> let outty_box = match outty_opt with @@ -189,17 +180,17 @@ let pp_ast0 t k = hbox false false [ builtin_symbol "["; hd ] :: aux_patterns tl in - add_level_info Ast.simple_prec Ast.simple_assoc + add_level_info Ast.simple_prec (hvbox false false [ hvbox false false ([match_box]); break; hbox false false [ hvbox false false patterns'' ] ]) | Ast.Cast (bo, ty) -> - add_level_info Ast.simple_prec Ast.simple_assoc + add_level_info Ast.simple_prec (hvbox false true [ builtin_symbol "("; top_pos (k bo); break; builtin_symbol ":"; top_pos (k ty); builtin_symbol ")"]) | Ast.LetIn (var, s, t) -> - add_level_info Ast.let_in_prec Ast.let_in_assoc + add_level_info Ast.let_in_prec (hvbox false true [ hvbox false true [ keyword "let"; space; @@ -251,7 +242,7 @@ let pp_ast0 t k = [ builtin_symbol "\\def"; break; body ])]) tl_funs in - add_level_info Ast.let_in_prec Ast.let_in_assoc + add_level_info Ast.let_in_prec ((hvbox false false (fst_row :: List.flatten tl_rows @ [ break; keyword "in"; break; k where ]))) @@ -330,7 +321,14 @@ let instantiate21 idrefs env l1 = (* following assertion should be a conditional that makes this * instantiation fail *) assert (CicNotationEnv.well_typed expected_ty value); - [ add_pos_info pos (CicNotationEnv.term_of_value value) ] + let value = CicNotationEnv.term_of_value value in + let value = + match expected_ty with + | Env.TermType (Some l) -> + Ast.AttributedTerm (`Level l,value) + | _ -> value + in + [ value ] | Ast.Magic m -> subst_magic pos env m | Ast.Literal l as t -> let t = add_idrefs idrefs t in @@ -470,15 +468,18 @@ let fill_pos_info l1_pattern = l1_pattern aux true l1_pattern *) let counter = ref ~-1 -let reset () = counter := ~-1;; +let reset () = + counter := ~-1; + Hashtbl.clear level1_patterns21 +;; let fresh_id = fun () -> incr counter; !counter -let add_pretty_printer ~precedence ~associativity l2 l1 = +let add_pretty_printer l2 (CicNotationParser.CL1P (l1,precedence)) = let id = fresh_id () in - let l1' = add_level_info precedence associativity (fill_pos_info l1) in + let l1' = add_level_info precedence (fill_pos_info l1) in let l2' = CicNotationUtil.strip_attributes l2 in Hashtbl.add level1_patterns21 id l1'; pattern21_matrix := (l2', id) :: !pattern21_matrix; @@ -542,7 +543,7 @@ let instantiate_level2 env term = new_name in let rec aux env term = -(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *) +(* prerr_endline ("ENV " ^ CicNotationPp.pp_env env); *) match term with | Ast.AttributedTerm (_, term) -> aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) @@ -593,7 +594,10 @@ let instantiate_level2 env term = and aux_variable env = function | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0) | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None) - | Ast.TermVar name -> Env.lookup_term env name + | Ast.TermVar (name,None) -> + Env.lookup_term env name + | Ast.TermVar (name,Some l) -> + Ast.AttributedTerm (`Level l,Env.lookup_term env name) | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None) | Ast.Ascription (term, name) -> assert false and aux_magic env = function @@ -634,7 +638,7 @@ let instantiate_level2 env term = | Env.ListValue (_ :: _) -> instantiate_fold_left (let acc_binding = - acc_name, (Env.TermType, Env.TermValue acc) + acc_name, (Env.TermType None, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern) (tail_names names env') @@ -656,7 +660,7 @@ let instantiate_level2 env term = | Env.ListValue (_ :: _) -> let acc = instantiate_fold_right (tail_names names env') in let acc_binding = - acc_name, (Env.TermType, Env.TermValue acc) + acc_name, (Env.TermType None, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern | Env.ListValue [] -> aux env base_pattern