X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=013e3a872fabcff73824e786fcae9982b52c2a4a;hb=b637879a2b3f2ceda65afb3c950061189c4730b7;hp=1ee406623ad91e61fab3745cef335e9636499d13;hpb=6719c0e318b312b51b089fea3d69d1b7103245ea;p=helm.git diff --git a/helm/software/components/content_pres/termContentPres.ml b/helm/software/components/content_pres/termContentPres.ml index 1ee406623..013e3a872 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 @@ -107,23 +98,22 @@ let pp_ast0 t k = let rec aux = function | Ast.Appl ts -> - let rec aux_args pos = + let rec aux_args level = function | [] -> [] | [ last ] -> - let last = k last in - if pos = `Left then [ left_pos last ] else [ right_pos last ] + [ Ast.AttributedTerm (`Level level,k last) ] | hd :: tl -> - (add_pos_info pos (k hd)) :: aux_args `Inner tl + (Ast.AttributedTerm (`Level level, k hd)) :: aux_args 71 tl in - add_level_info Ast.apply_prec Ast.apply_assoc - (hovbox true true (CicNotationUtil.dress break (aux_args `Left ts))) + add_level_info Ast.apply_prec + (hovbox true true (CicNotationUtil.dress break (aux_args 70 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,24 +179,24 @@ 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; hvbox false true [ aux_var var; space; builtin_symbol "\\def"; break; top_pos (k s) ]; - break; space; keyword "in" ]; + break; space; keyword "in"; space ]; break; k t ]) | Ast.LetRec (rec_kind, funs, where) -> @@ -251,7 +241,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 +320,13 @@ 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 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 @@ -350,7 +346,7 @@ let instantiate21 idrefs env l1 = let sep = match sep_opt with | None -> [] - | Some l -> [ Ast.Literal l ] + | Some l -> [ Ast.Literal l; break; space ] in let rec instantiate_list acc = function | [] -> List.rev acc @@ -363,7 +359,7 @@ let instantiate21 idrefs env l1 = let terms = subst pos env p in instantiate_list (CicNotationUtil.group (terms @ sep) :: acc) tl in - instantiate_list [] values + [hovbox false false (instantiate_list [] values)] | Ast.Opt p -> let opt_decls = CicNotationEnv.declarations_of_term p in let env = @@ -470,15 +466,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; @@ -512,6 +511,8 @@ let head_names names env = (match ty, v with | Env.ListType ty, Env.ListValue (v :: _) -> aux ((name, (ty, v)) :: acc) tl + | Env.TermType _, Env.TermValue _ -> + aux ((name, (ty, v)) :: acc) tl | _ -> assert false) | _ :: tl -> aux acc tl (* base pattern may contain only meta names, thus we trash all others *) @@ -525,6 +526,8 @@ let tail_names names env = (match ty, v with | Env.ListType ty, Env.ListValue (_ :: vtl) -> aux ((name, (Env.ListType ty, Env.ListValue vtl)) :: acc) tl + | Env.TermType _, Env.TermValue _ -> + aux ((name, (ty, v)) :: acc) tl | _ -> assert false) | binding :: tl -> aux (binding :: acc) tl | [] -> acc @@ -532,6 +535,7 @@ let tail_names names env = aux [] env let instantiate_level2 env term = +(* prerr_endline ("istanzio: " ^ CicNotationPp.pp_term term); *) let fresh_env = ref [] in let lookup_fresh_name n = try @@ -542,9 +546,9 @@ 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.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms) | Ast.Binder (binder, var, body) -> Ast.Binder (binder, aux_capture_var env var, aux env body) @@ -593,7 +597,8 @@ 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,(Ast.Level l|Ast.Self 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 +639,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 0, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern) (tail_names names env') @@ -656,7 +661,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 0, Env.TermValue acc) in aux (acc_binding :: head_names names env') rec_pattern | Env.ListValue [] -> aux env base_pattern